Theorem aleximi 1855

Description: A variant of al2imi 1838: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2188, sps 2223 and eximd 2254, 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

Step	Hyp	Ref	Expression
1		aleximi.1	. . . . 5 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	con3d 153	. . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	al2imi 1838	. . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4		alnex 1804	. . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5		alnex 1804	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
6	3, 4, 5	3imtr3g 298	. 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
7	6	con4d 116	1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1561  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  alexbii  1856  exim  1857  eximdh  1887  19.29  1896  19.29r  1897  19.35  1900  19.25  1903  19.30  1904  19.40b  1911  exintr  1915  19.36imv  1968  speimfw  1986  aeveq  2081  sbequ2  2287  2ax6elem  2504  sb1  2512  dfeumo  2566  mo3  2594  mo4  2596  mopick  2655  2mo  2678  ssel  3933  ssrexv  4009  axprlem4  5388  ssopab2  5522  ssoprab2  7468  elirrv  9547  axextnd  10564  axnulregtco  36853  bj-2exim  37085  bj-exalimi  37100  bj-eximcom  37101  bj-subst  37145  bj-gabss  37432  wl-mo3t  38091  wl-eujustlem1  38103  pm10.56  44944  2exim  44953