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

Theorem aleximi 1756
Description: A variant of al2imi 1740: instead of applying 𝑥 quantifiers to the final implication, replace them with 𝑥. A shorter proof is possible using nfa1 2025, sps 2053 and eximd 2083, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.)
Hypothesis
Ref Expression
aleximi.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
aleximi (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Proof of Theorem aleximi
StepHypRef Expression
1 aleximi.1 . . . . 5 (𝜑 → (𝜓𝜒))
21con3d 148 . . . 4 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32al2imi 1740 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1703 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1703 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 284 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 114 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  alexbii  1757  exim  1758  exanOLD  1786  eximdh  1788  19.29  1798  19.29r  1799  19.35  1802  19.25  1805  19.30  1806  19.40b  1812  speimfw  1873  aeveq  1979  aevOLD  2159  2ax6elem  2448  mo3  2506  mopick  2534  2mo  2550  ssopab2  4961  ssoprab2  6664  axextnd  9357  bj-2exim  32237  bj-exalimi  32254  bj-sb56  32281  wl-dveeq12  32943  wl-mo3t  32990  pm10.56  38051  2exim  38060
  Copyright terms: Public domain W3C validator