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

Theorem aleximi 1908
 Description: A variant of al2imi 1892: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2177, sps 2202 and eximd 2232, 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 1892 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1855 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1855 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 284 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 114 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1630  ∃wex 1853 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886 This theorem depends on definitions:  df-bi 197  df-ex 1854 This theorem is referenced by:  alexbii  1909  exim  1910  exanOLD  1938  eximdh  1940  19.29  1950  19.29r  1951  19.35  1954  19.25  1957  19.30  1958  19.40b  1964  speimfw  2042  aeveq  2133  2ax6elem  2586  mo3  2645  mopick  2673  2mo  2689  ssopab2  5151  ssoprab2  6876  axextnd  9605  bj-2exim  32901  bj-exalimi  32918  bj-sb56  32945  wl-dveeq12  33624  wl-mo3t  33671  pm10.56  39071  2exim  39080
 Copyright terms: Public domain W3C validator