theorem Th46: :: AOFA_L00:47

for n being non empty Nat
for S being non empty non void b₁ 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 st C \imp (B \imp A) in F & B in F holds
C \imp A in F