Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axc5c711 Structured version   Visualization version   GIF version

Theorem axc5c711 35934
Description: Proof of a single axiom that can replace ax-c5 35899, ax-c7 35901, and ax-11 2151 in a subsystem that includes these axioms plus ax-c4 35900 and ax-gen 1787 (and propositional calculus). See axc5c711toc5 35935, axc5c711toc7 35936, and axc5c711to11 35937 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 35927. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
axc5c711 ((∀𝑥𝑦 ¬ ∀𝑥𝑦𝜑 → ∀𝑥𝜑) → 𝜑)

Proof of Theorem axc5c711
StepHypRef Expression
1 ax-c5 35899 . . 3 (∀𝑦𝜑𝜑)
2 ax10fromc7 35911 . . . 4 (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑)
3 ax-c7 35901 . . . . . 6 (¬ ∀𝑥 ¬ ∀𝑥𝑦𝜑 → ∀𝑦𝜑)
43con1i 149 . . . . 5 (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥𝑦𝜑)
54alimi 1803 . . . 4 (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦𝑥 ¬ ∀𝑥𝑦𝜑)
6 ax-11 2151 . . . 4 (∀𝑦𝑥 ¬ ∀𝑥𝑦𝜑 → ∀𝑥𝑦 ¬ ∀𝑥𝑦𝜑)
72, 5, 63syl 18 . . 3 (¬ ∀𝑦𝜑 → ∀𝑥𝑦 ¬ ∀𝑥𝑦𝜑)
81, 7nsyl4 161 . 2 (¬ ∀𝑥𝑦 ¬ ∀𝑥𝑦𝜑𝜑)
9 ax-c5 35899 . 2 (∀𝑥𝜑𝜑)
108, 9ja 187 1 ((∀𝑥𝑦 ¬ ∀𝑥𝑦𝜑 → ∀𝑥𝜑) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-11 2151  ax-c5 35899  ax-c4 35900  ax-c7 35901
This theorem is referenced by:  axc5c711toc5  35935  axc5c711toc7  35936  axc5c711to11  35937
  Copyright terms: Public domain W3C validator