Theorem wl-section-prop 35516

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

Alternatively, I start from Jan Lukasiewicz's axiom system here, i.e., ax-mp 5, ax-luk1 35517, ax-luk2 35518 and ax-luk3 35519. I rather copy this system than use luk-1 1659 to luk-3 1661, 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.)

Hypothesis

Ref	Expression
wl-section-prop.hyp	⊢ 𝜑

Assertion

Ref	Expression
wl-section-prop	⊢ 𝜑

Proof of Theorem wl-section-prop

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

This theorem is referenced by: (None)