Next Prev Up
LeftChopChopImpChopRule

⊢ f ; g ⊃ g ⇒ ⊢ f ; g ; h ⊃ g ; h LeftChopChopImpChopRule

Proof:

1
⊢ f ; g ⊃ g
given
2
⊢ (f ; g) ; h ⊃ g ; h
1,LeftChopImpChop
3
⊢ (f ; g) ; h ≡ f ; g ; h
ChopAssoc
4
⊢ f ; g ; h ⊃ g ; h
2, 3,Prop

qed

Next Prev Up

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