Prev Up
ChopPlusEqvChopPlus

⊢ f ≡ g ⇒ ⊢ f+ ≡ g+ ChopPlusEqvChopPlus

Proof:

1
⊢ f ≡ g
given
2
⊢ f ⊃ g
1,Prop
3
⊢ f+ ⊃ g+
2,ChopPlusImpChopPlus
4
⊢ g ⊃ f
1,Prop
5
⊢ g+ ⊃ f+
4,ChopPlusImpChopPlus
6
⊢ f+ ≡ g+
3, 5,Prop

qed

Prev Up

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