Next Prev Up
RightChopEqvChop

⊢ g ≡ g1 ⇒ ⊢ (f ⌢ g) ≡ (f ⌢ g1) RightChopEqvChop

Proof:

1
g ≡ g1
Assump
2
g ⊃ g1
1,Prop
3
f ⌢ g ⊃ f ⌢ g1
2,RightChopImpChop
4
g1 ⊃ g
1,Prop
5
f ⌢ g1 ⊃ f ⌢ g
4,RightChopImpChop
6
f ⌢ g ≡ f ⌢ g1
3, 5,Prop

qed

Next Prev Up

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