Next Prev Up
ChopImpDi

⊢ f ; g ⊃ f ChopImpDi

Proof:

1
⊢ g ⊃true
Prop
2
⊢ f ; g ⊃ f ; true
1,BoxChopImpChop
3
⊢ f ; g ⊃ f
2, def. of 

qed

Next Prev Up

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