BiImpDist

BiImpDist

⊢

(f ⊃ g) ⊃ (

f) ⊃ (

g)

BiImpDist

Proof:

1	⊢ (f ⊃ g) ⊃ (¬g ⊃ ¬f)	Prop
2	⊢ ¬(¬g ⊃ ¬f) ⊃¬(f ⊃ g)	1,Prop
3	⊢ (¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g))	2,BiGen
4	⊢ (¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g)) ⊃
	(f ⊃ g) ⊃ (¬g ⊃ ¬f)	BiContraPosImpDist
5	⊢ (f ⊃ g) ⊃ (¬g ⊃ ¬f)	3, 4,MP
6	⊢ (¬g ⊃ ¬f) ⊃ ( f) ⊃ ( g)	BiContraPosImpDist
7	⊢ (f ⊃ g) ⊃ ( f) ⊃ ( g)	5, 6,ImpChain

qed

2024-08-03

Contact | Home | ITL home | Course | Proofs | Algebra | FL

© 1996-2024