Theorem aleximi 1827

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1532  ∃wex 1774

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

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  alexbii  1828  exim  1829  eximdh  1860  19.29  1869  19.29r  1870  19.35  1873  19.25  1876  19.30  1877  19.40b  1884  exintr  1888  19.36imv  1941  speimfw  1960  aeveq  2052  sbequ2  2234  2ax6elem  2464  sb1  2472  dfeumo  2526  mo3  2553  mo4  2555  mopick  2616  2mo  2639  ssel  3971  ssopab2  5542  ssoprab2  7482  axextnd  10606  bj-2exim  36024  bj-exalimi  36045  bj-cbvalimt  36051  bj-eximcom  36055  bj-subst  36073  bj-gabss  36349  wl-mo3t  36978  pm10.56  43730  2exim  43739