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

Theorem aleximi 1828
 Description: A variant of al2imi 1812: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2151, sps 2179 and eximd 2211, 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 1812 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1778 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1778 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 297 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 115 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1531  ∃wex 1776 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806 This theorem depends on definitions:  df-bi 209  df-ex 1777 This theorem is referenced by:  alexbii  1829  exim  1830  eximdh  1861  19.29  1870  19.29r  1871  19.35  1874  19.25  1877  19.30  1878  19.40b  1885  exintr  1889  speimfw  1962  aeveq  2057  sbequ2  2245  2ax6elem  2489  sb1  2499  dfeumo  2615  mo3  2644  mo4  2646  mopick  2706  2mo  2729  ssopab2  5426  ssoprab2  7216  axextnd  10007  bj-2exim  33940  bj-exalimi  33961  bj-cbvalimt  33967  bj-eximcom  33971  bj-sb56  33989  wl-mo3t  34806  pm10.56  40695  2exim  40704
 Copyright terms: Public domain W3C validator