Theorem aleximi 1851

Description: A variant of al2imi 1834: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2184, sps 2219 and eximd 2250, 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 152	. . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	al2imi 1834	. . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4		alnex 1800	. . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5		alnex 1800	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
6	3, 4, 5	3imtr3g 297	. 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
7	6	con4d 115	1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  alexbii  1852  exim  1853  eximdh  1883  19.29  1892  19.29r  1893  19.35  1896  19.25  1899  19.30  1900  19.40b  1907  exintr  1911  19.36imv  1964  speimfw  1982  aeveq  2077  sbequ2  2283  2ax6elem  2500  sb1  2508  dfeumo  2562  mo3  2590  mo4  2592  mopick  2651  2mo  2674  ssel  3930  ssrexv  4006  axprlem4  5382  ssopab2  5515  ssoprab2  7460  elirrv  9542  axextnd  10546  axnulregtco  36804  bj-2exim  37037  bj-exalimi  37052  bj-eximcom  37053  bj-subst  37097  bj-gabss  37384  wl-mo3t  38043  wl-eujustlem1  38055  pm10.56  44910  2exim  44919