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

Theorem aleximi 1827
Description: A variant of al2imi 1810: instead of applying 𝑥 quantifiers to the final implication, replace them with 𝑥. A shorter proof is possible using nfa1 2141, sps 2171 and eximd 2202, 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 152 . . . 4 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32al2imi 1810 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1776 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1776 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 295 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 115 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1532  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-ex 1775
This theorem is referenced by:  alexbii  1828  exim  1829  eximdh  1860  19.29  1869  19.29r  1870  19.35  1873  19.25  1876  19.30  1877  19.40b  1884  exintr  1888  19.36imv  1941  speimfw  1960  aeveq  2052  sbequ2  2234  2ax6elem  2464  sb1  2472  dfeumo  2526  mo3  2553  mo4  2555  mopick  2616  2mo  2639  ssel  3971  ssopab2  5542  ssoprab2  7482  axextnd  10606  bj-2exim  36024  bj-exalimi  36045  bj-cbvalimt  36051  bj-eximcom  36055  bj-subst  36073  bj-gabss  36349  wl-mo3t  36978  pm10.56  43730  2exim  43739
  Copyright terms: Public domain W3C validator