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  2468  sb1  2476  dfeumo  2530  mo3  2557  mo4  2559  mopick  2618  2mo  2641  ssel  3931  ssrexv  4007  axprlem4  5368  ssopab2  5493  ssoprab2  7421  axextnd  10504  bj-2exim  36584  bj-exalimi  36606  bj-cbvalimt  36612  bj-eximcom  36616  bj-subst  36634  bj-gabss  36908  wl-mo3t  37549  pm10.56  44343  2exim  44352