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  3940  ssrexv  4016  axprlem4  5381  ssopab2  5506  ssoprab2  7457  axextnd  10544  bj-2exim  36599  bj-exalimi  36621  bj-cbvalimt  36627  bj-eximcom  36631  bj-subst  36649  bj-gabss  36923  wl-mo3t  37564  pm10.56  44359  2exim  44368