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

Theorem aleximi 1823
Description: A variant of al2imi 1807: instead of applying 𝑥 quantifiers to the final implication, replace them with 𝑥. A shorter proof is possible using nfa1 2146, sps 2174 and eximd 2206, 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 1807 . . 3 (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4 alnex 1773 . . 3 (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5 alnex 1773 . . 3 (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
63, 4, 53imtr3g 296 . 2 (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
76con4d 115 1 (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  alexbii  1824  exim  1825  eximdh  1856  19.29  1865  19.29r  1866  19.35  1869  19.25  1872  19.30  1873  19.40b  1880  exintr  1884  speimfw  1957  aeveq  2052  sbequ2  2240  2ax6elem  2485  sb1  2496  dfeumo  2612  mo3  2641  mo4  2643  mopick  2703  2mo  2726  ssopab2  5424  ssoprab2  7211  axextnd  10001  bj-2exim  33842  bj-exalimi  33863  bj-cbvalimt  33869  bj-eximcom  33873  bj-sb56  33891  wl-mo3t  34693  pm10.56  40579  2exim  40588
  Copyright terms: Public domain W3C validator