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

Theorem aleximi 1926
Description: A variant of al2imi 1910: instead of applying 𝑥 quantifiers to the final implication, replace them with 𝑥. A shorter proof is possible using nfa1 2193, sps 2217 and eximd 2249, 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 149 . . . 4 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32al2imi 1910 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1876 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1876 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 286 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 115 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1650  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-ex 1875
This theorem is referenced by:  alexbii  1927  exim  1928  alexan  1959  eximdh  1961  19.29  1972  19.29r  1973  19.35  1976  19.25  1979  19.30  1980  19.40b  1986  speimfw  2058  aeveq  2149  nfeqf2  2396  2ax6elem  2541  mo3  2628  mopick  2657  2mo  2673  ssopab2  5162  ssoprab2  6909  axextnd  9666  bj-2exim  33031  bj-exalimi  33048  bj-sb56  33075  wl-mo3t  33783  pm10.56  39243  2exim  39252
  Copyright terms: Public domain W3C validator