let n be non empty Nat; :: thesis: for S being non empty non void n PC-correct PCLangSignature

for L being language MSAlgebra over S

for F being PC-theory of L

for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let S be non empty non void n PC-correct PCLangSignature ; :: thesis: for L being language MSAlgebra over S

for F being PC-theory of L

for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L

for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let F be PC-theory of L; :: thesis: for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let A, B, C, D be Formula of L; :: thesis: ( A \imp B in F & C \imp D in F implies (B \imp C) \imp (A \imp D) in F )

assume ( A \imp B in F & C \imp D in F ) ; :: thesis: (B \imp C) \imp (A \imp D) in F

then ( (B \imp C) \imp (A \imp C) in F & (A \imp C) \imp (A \imp D) in F ) by Th101, Th102;

hence (B \imp C) \imp (A \imp D) in F by Th45; :: thesis: verum

for L being language MSAlgebra over S

for F being PC-theory of L

for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let S be non empty non void n PC-correct PCLangSignature ; :: thesis: for L being language MSAlgebra over S

for F being PC-theory of L

for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L

for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let F be PC-theory of L; :: thesis: for A, B, C, D being Formula of L st A \imp B in F & C \imp D in F holds

(B \imp C) \imp (A \imp D) in F

let A, B, C, D be Formula of L; :: thesis: ( A \imp B in F & C \imp D in F implies (B \imp C) \imp (A \imp D) in F )

assume ( A \imp B in F & C \imp D in F ) ; :: thesis: (B \imp C) \imp (A \imp D) in F

then ( (B \imp C) \imp (A \imp C) in F & (A \imp C) \imp (A \imp D) in F ) by Th101, Th102;

hence (B \imp C) \imp (A \imp D) in F by Th45; :: thesis: verum