Theorem aleximi 1831

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1778

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

This theorem depends on definitions:  df-bi 207  df-ex 1779

This theorem is referenced by:  alexbii  1832  exim  1833  eximdh  1863  19.29  1872  19.29r  1873  19.35  1876  19.25  1879  19.30  1880  19.40b  1887  exintr  1891  19.36imv  1944  speimfw  1962  aeveq  2055  sbequ2  2248  2ax6elem  2474  sb1  2482  dfeumo  2536  mo3  2563  mo4  2565  mopick  2624  2mo  2647  ssel  3976  ssrexv  4052  axprlem4  5425  ssopab2  5550  ssoprab2  7502  axextnd  10632  bj-2exim  36613  bj-exalimi  36635  bj-cbvalimt  36641  bj-eximcom  36645  bj-subst  36663  bj-gabss  36937  wl-mo3t  37578  pm10.56  44394  2exim  44403