Next Prev Up
ChopImpDiamond

⊢ f ; g ⊃ g ChopImpDiamond

Proof:

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

qed

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024