Next Prev Up
LeftChopEqvChop

⊢ f ≡ f1 ⇒ ⊢ (f ⌢ g) ≡ (f1 ⌢ g) LeftChopEqvChop

Proof:

1
f ≡ f1
Assump
2
f ⊃ f1
1,Prop
3
f ⌢ g ⊃ f1 ⌢ g
2,LeftChopImpChop
4
f1 ⊃ f
1,Prop
5
f1 ⌢ g ⊃ f ⌢ g
4,LeftChopImpChop
6
f ⌢ g ≡ f1 ⌢ g
3, 5,Prop

qed

Next Prev Up

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