Next Prev Up
FRightSkipChopImpSkipChopRule

⊢ f ⊃ g ⇒ ⊢ ⟨skip⟩f ⊃ ⟨skip⟩g FRightSkipChopImpSkipChopRule

Proof:

1
f ⊃ g
Assump
2
(f ⊃ g)
FLBoxGen
3
(f ⊃ g) ⊃ ⟨skip⟩f ⊃ ⟨skip⟩g
FL9
4
⟨skip⟩f ⊃ ⟨skip⟩g
2, 3,MP

qed

Next Prev Up

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