Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-section-prop Structured version   Visualization version   GIF version

Theorem wl-section-prop 34581
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 34582, ax-luk2 34583 and ax-luk3 34584. I rather copy this system than use luk-1 1647 to luk-3 1649, 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
StepHypRef Expression
1 wl-section-prop.hyp 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator