Users' Mathboxes Mathbox for Adhemar < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  adh-minim-ax1 Structured version   Visualization version   GIF version

Theorem adh-minim-ax1 46447
Description: Derivation of ax-1 6 from adh-minim 46442 and ax-mp 5. Carew Arthur Meredith derived ax-1 6 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CpCqp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
adh-minim-ax1 (𝜑 → (𝜓𝜑))

Proof of Theorem adh-minim-ax1
StepHypRef Expression
1 adh-minim-ax1-ax2-lem1 46443 . 2 (𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)) → (𝜓𝜑)))
2 adh-minim-ax1-ax2-lem1 46443 . . . 4 ((𝜓𝜑) → ((𝜓 → ((𝜂 → ((𝜁 → (𝜓𝜎)) → (𝜁𝜎))) → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))))
3 adh-minim-ax1-ax2-lem3 46445 . . . . 5 (((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → (𝜓𝜑)) → (𝜓 → ((𝜂 → ((𝜁 → (𝜓𝜎)) → (𝜁𝜎))) → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))))
4 adh-minim-ax1-ax2-lem4 46446 . . . . 5 ((((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → (𝜓𝜑)) → (𝜓 → ((𝜂 → ((𝜁 → (𝜓𝜎)) → (𝜁𝜎))) → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)))) → (((𝜓𝜑) → ((𝜓 → ((𝜂 → ((𝜁 → (𝜓𝜎)) → (𝜁𝜎))) → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)))) → ((𝜓𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)))))
53, 4ax-mp 5 . . . 4 (((𝜓𝜑) → ((𝜓 → ((𝜂 → ((𝜁 → (𝜓𝜎)) → (𝜁𝜎))) → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)))) → ((𝜓𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))))
62, 5ax-mp 5 . . 3 ((𝜓𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)))
7 adh-minim-ax1-ax2-lem4 46446 . . 3 (((𝜓𝜑) → (𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑))) → ((𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)) → (𝜓𝜑))) → (𝜑 → (𝜓𝜑))))
86, 7ax-mp 5 . 2 ((𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓𝜏)) → (𝜃𝜏))) → 𝜑)) → (𝜓𝜑))) → (𝜑 → (𝜓𝜑)))
91, 8ax-mp 5 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:  adh-minim-ax2-lem5  46448  adh-minim-idALT  46452  adh-minim-pm2.43  46453
  Copyright terms: Public domain W3C validator