FNextImpNextRule

⊢ f ⊃ g ⇒

f ⊃

FNextImpNextRule

Proof:

1	f ⊃ g	Assump
2	⟨skip⟩f ⊃ ⟨skip⟩g	1,FRightSkipChopImpSkipChopRule
3	f ≡⟨skip⟩f	FL2
4	g ≡⟨skip⟩g	FL2
5	f ⊃ g	3, 4,Prop

qed

2024-08-03