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 2191, sps 2225 and eximd 2256, 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  1908  19.29r  1909  19.35  1912  19.25  1915  19.30  1916  19.40b  1923  exintr  1927  19.36imv  1980  speimfw  1998  aeveq  2093  sbequ2  2288  2ax6elem  2502  sb1  2510  dfeumo  2564  mo3  2592  mo4  2594  mopick  2653  2mo  2676  ssel  3907  ssrexv  3983  axprlem4  5395  ssopab2  5528  ssoprab2  7519  elirrv  9628  axextnd  10715  axnulregtco  37483  bj-2exim  37715  bj-exalimi  37730  bj-eximcom  37731  bj-subst  37775  bj-gabss  38063  wl-mo3t  38776  wl-eujustlem1  38788  pm10.56  45615  2exim  45624