BfContraPosImpDist

⊢ (¬g ⊃ ¬f) ⊃ ( f) ⊃ ( g) BfContraPosImpDist

Proof:

1
(¬g ⊃ ¬f) ⊃ ( ¬g) ⊃ ( ¬f)
2
(¬g ⊃ ¬f) ⊃ (¬¬f) ⊃ (¬¬g)
1,Prop
3
(¬g ⊃ ¬f) ⊃ ( f) ⊃ ( g)
2, def. of 

qed

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024