MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minimp Structured version   Visualization version   GIF version

Theorem minimp 1628
Description: A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). (Contributed by BJ, 4-Apr-2021.)
Assertion
Ref Expression
minimp (𝜑 → ((𝜓𝜒) → (((𝜃𝜓) → (𝜒𝜏)) → (𝜓𝜏))))

Proof of Theorem minimp
StepHypRef Expression
1 jarr 106 . . . 4 (((𝜃𝜓) → (𝜒𝜏)) → (𝜓 → (𝜒𝜏)))
21a2d 29 . . 3 (((𝜃𝜓) → (𝜒𝜏)) → ((𝜓𝜒) → (𝜓𝜏)))
32com12 32 . 2 ((𝜓𝜒) → (((𝜃𝜓) → (𝜒𝜏)) → (𝜓𝜏)))
43a1i 11 1 (𝜑 → ((𝜓𝜒) → (((𝜃𝜓) → (𝜒𝜏)) → (𝜓𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  minimp-syllsimp  1629  minimp-ax2c  1631
  Copyright terms: Public domain W3C validator