Theorem aleximi 1832

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1538  ∃wex 1779

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

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

This theorem is referenced by:  alexbii  1833  exim  1834  eximdh  1864  19.29  1873  19.29r  1874  19.35  1877  19.25  1880  19.30  1881  19.40b  1888  exintr  1892  19.36imv  1945  speimfw  1963  aeveq  2057  sbequ2  2250  2ax6elem  2475  sb1  2483  dfeumo  2537  mo3  2564  mo4  2566  mopick  2625  2mo  2648  ssel  3957  ssrexv  4033  axprlem4  5401  ssopab2  5526  ssoprab2  7480  axextnd  10610  bj-2exim  36634  bj-exalimi  36656  bj-cbvalimt  36662  bj-eximcom  36666  bj-subst  36684  bj-gabss  36958  wl-mo3t  37599  pm10.56  44369  2exim  44378