BiImpBiRule

⊢ f ⊃ g ⇒ ⊢ f ⊃ g BiImpBiRule

Proof:

1
⊢ f ⊃ g
given
2
⊢ ¬g ⊃¬f
1,Prop
3
⊢ ¬g ⊃¬f
4
⊢ ¬¬f ⊃¬¬g
3,Prop
5
⊢ f ⊃ g
4, def. of 

qed

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