Theorem wl-section-prop

Description: Intuitionistic logic is now developed separately, so we need not first focus on intuitionally valid axioms ax-1 and ax-2 any longer.

Alternatively, I start from Jan Lukasiewicz's axiom system here, i.e., ax-mp , ax-luk1 , ax-luk2 and ax-luk3 . I rather copy this system than use luk-1 to luk-3 , since the latter are theorems, while we need axioms here.

(Contributed by Wolf Lammen, 23-Feb-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	wl-section-prop.hyp	⊢ 𝜑
Assertion	wl-section-prop	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		wl-section-prop.hyp	⊢ 𝜑