Theorem aleximi 1829

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1535  ∃wex 1776

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

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

This theorem is referenced by:  alexbii  1830  exim  1831  eximdh  1862  19.29  1871  19.29r  1872  19.35  1875  19.25  1878  19.30  1879  19.40b  1886  exintr  1890  19.36imv  1943  speimfw  1961  aeveq  2054  sbequ2  2247  2ax6elem  2473  sb1  2481  dfeumo  2535  mo3  2562  mo4  2564  mopick  2623  2mo  2646  ssel  3989  ssrexv  4065  axprlem4  5432  ssopab2  5556  ssoprab2  7501  axextnd  10629  bj-2exim  36594  bj-exalimi  36616  bj-cbvalimt  36622  bj-eximcom  36626  bj-subst  36644  bj-gabss  36918  wl-mo3t  37557  pm10.56  44366  2exim  44375