Next Up
FiniteImpBfImpBfRule

⊢ finite ⊃ (f ⊃ g) ⇒ ⊢ f ⊃ g FiniteImpBfImpBfRule

Proof:

1
finite ⊃ (f ⊃ g)
Assump
2
(f ⊃ g)
1,BfFGen
3
(f ⊃ g) ⊃ ( f ⊃ g)
BfImpDist
4
f ⊃ g
2, 3,MP

qed

Next Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023