Next Prev Up
BoxImpInferBoxImpBox

⊢ f ⊃ g ⇒ ⊢ f ⊃ g BoxImpInferBoxImpBox

Proof:

1
f ⊃ g
Assump
2
( f ⊃ g)
1,BoxGen
3
( f ⊃ g) ⊃ ( f ⊃ g)
VPTL
4
f ⊃ g
2, 3,MP

qed

Next Prev Up

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