Theorem aleximi 1862

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  alexbii  1863  exim  1864  eximdh  1894  19.29  1903  19.29r  1904  19.35  1907  19.25  1910  19.30  1911  19.40b  1918  exintr  1922  19.36imv  1975  speimfw  1993  aeveq  2088  sbequ2  2285  2ax6elem  2502  sb1  2510  dfeumo  2564  mo3  2592  mo4  2594  mopick  2653  2mo  2676  ssel  3932  ssrexv  4008  axprlem4  5399  ssopab2  5533  ssoprab2  7480  elirrv  9560  axextnd  10577  axnulregtco  36972  bj-2exim  37204  bj-exalimi  37219  bj-eximcom  37220  bj-subst  37264  bj-gabss  37552  wl-mo3t  38212  wl-eujustlem1  38224  pm10.56  45063  2exim  45072