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

Theorem aleximi 1839
Description: A variant of al2imi 1823: instead of applying 𝑥 quantifiers to the final implication, replace them with 𝑥. A shorter proof is possible using nfa1 2153, sps 2183 and eximd 2215, 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 155 . . . 4 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32al2imi 1823 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1789 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1789 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 298 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 115 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1541  wex 1787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817
This theorem depends on definitions:  df-bi 210  df-ex 1788
This theorem is referenced by:  alexbii  1840  exim  1841  eximdh  1872  19.29  1881  19.29r  1882  19.35  1885  19.25  1888  19.30  1889  19.40b  1896  exintr  1900  19.36imv  1953  speimfw  1972  aeveq  2063  sbequ2  2247  2ax6elem  2470  sb1  2479  dfeumo  2537  mo3  2564  mo4  2566  mopick  2627  2mo  2650  ssel  3907  ssopab2  5441  ssoprab2  7297  axextnd  10229  bj-2exim  34556  bj-exalimi  34577  bj-cbvalimt  34583  bj-eximcom  34587  bj-subst  34605  bj-gabss  34886  wl-mo3t  35494  pm10.56  41689  2exim  41698
  Copyright terms: Public domain W3C validator