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

Prev Up

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