Theorem aleximi 1865

Description: A variant of al2imi 1848: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2188, sps 2221 and eximd 2252, 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 1848	. . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4		alnex 1814	. . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5		alnex 1814	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
6	3, 4, 5	3imtr3g 298	. 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
7	6	con4d 116	1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  alexbii  1866  exim  1867  eximdh  1897  19.29  1906  19.29r  1907  19.35  1910  19.25  1913  19.30  1914  19.40b  1921  exintr  1925  19.36imv  1978  speimfw  1996  aeveq  2091  sbequ2  2284  2ax6elem  2499  sb1  2507  dfeumo  2561  mo3  2589  mo4  2591  mopick  2650  2mo  2673  ssel  3925  ssrexv  4001  axprlem4  5391  ssopab2  5525  ssoprab2  7481  elirrv  9569  axextnd  10600  axnulregtco  37099  bj-2exim  37331  bj-exalimi  37346  bj-eximcom  37347  bj-subst  37391  bj-gabss  37679  wl-mo3t  38339  wl-eujustlem1  38351  pm10.56  45194  2exim  45203