StateImpYields

⊢ w ∧ f ⊃ fin w1 ⇒ ⊢ w ⊃ (f w1) StateImpYields

Proof:

1
⊢ w ∧ f ⊃fin w1
given
2
⊢ w ⊃ (f ⊃ fin w1)
1,Prop
3
⊢ w ⊃ (f ⊃ fin w1)
4
⊢ (f ⊃ fin w1) ≡ f w1
5
⊢ w ⊃ (f w1)
3, 4,EqvChain

qed

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024