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 being Formula of L holds (B \imp C) \imp ((A \imp B) \imp (A \imp C)) 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 being Formula of L holds (B \imp C) \imp ((A \imp B) \imp (A \imp C)) in F
let L be language MSAlgebra over S; :: thesis: for F being PC-theory of L
for A, B, C being Formula of L holds (B \imp C) \imp ((A \imp B) \imp (A \imp C)) in F
let F be PC-theory of L; :: thesis: for A, B, C being Formula of L holds (B \imp C) \imp ((A \imp B) \imp (A \imp C)) in F
let A, B, C be Formula of L; :: thesis: (B \imp C) \imp ((A \imp B) \imp (A \imp C)) in F
A1: (A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)) in F by Def38;
A2: ((B \imp C) \imp ((A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)))) \imp (((B \imp C) \imp (A \imp (B \imp C))) \imp ((B \imp C) \imp ((A \imp B) \imp (A \imp C)))) in F by Def38;
((A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C))) \imp ((B \imp C) \imp ((A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C)))) in F by Def38;
then (B \imp C) \imp ((A \imp (B \imp C)) \imp ((A \imp B) \imp (A \imp C))) in F by A1, Def38;
then A3: ((B \imp C) \imp (A \imp (B \imp C))) \imp ((B \imp C) \imp ((A \imp B) \imp (A \imp C))) in F by A2, Def38;
(B \imp C) \imp (A \imp (B \imp C)) in F by Def38;
hence (B \imp C) \imp ((A \imp B) \imp (A \imp C)) in F by A3, Def38; :: thesis: verum