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

Theorem aleximi 1757
Description: A variant of al2imi 1741: instead of applying 𝑥 quantifiers to the final implication, replace them with 𝑥. A shorter proof is possible using nfa1 2026, 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 1741 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1704 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1704 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 284 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 114 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  alexbii  1758  exim  1759  exanOLD  1787  eximdh  1789  19.29  1799  19.29r  1800  19.35  1803  19.25  1806  19.30  1807  19.40b  1813  speimfw  1874  aeveq  1980  aevOLD  2160  2ax6elem  2447  mo3  2505  mopick  2533  2mo  2549  ssopab2  4991  ssoprab2  6696  axextnd  9398  bj-2exim  32570  bj-exalimi  32587  bj-sb56  32614  wl-dveeq12  33282  wl-mo3t  33329  pm10.56  38389  2exim  38398
  Copyright terms: Public domain W3C validator