BfImpDist

BfImpDist

⊢

(f ⊃ g) ⊃ (

f) ⊃ (

g)

BfImpDist

Proof:

1	(f ⊃ g) ⊃ (¬g ⊃ ¬f)	Prop
2	¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g)	1,Prop
3	(¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g))	2,BfGen
4	(¬(¬g ⊃ ¬f) ⊃ ¬(f ⊃ g))
	⊃ (f ⊃ g) ⊃ (¬g ⊃ ¬f)	BfContraPosImpDist
5	(f ⊃ g) ⊃ (¬g ⊃ ¬f)	3, 4,MP
6	(¬g ⊃ ¬f) ⊃ ( f) ⊃ ( g)	BfContraPosImpDist
7	(f ⊃ g) ⊃ ( f) ⊃ ( g)	5, 6,ImpChain

qed

2023-09-12

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

© 1996-2023