Theorem aleximi 1864

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  alexbii  1865  exim  1866  eximdh  1896  19.29  1905  19.29r  1906  19.35  1909  19.25  1912  19.30  1913  19.40b  1920  exintr  1924  19.36imv  1977  speimfw  1995  aeveq  2090  sbequ2  2284  2ax6elem  2499  sb1  2507  dfeumo  2561  mo3  2589  mo4  2591  mopick  2650  2mo  2673  ssel  3902  ssrexv  3978  axprlem4  5387  ssopab2  5520  ssoprab2  7489  elirrv  9595  axextnd  10680  axnulregtco  37361  bj-2exim  37593  bj-exalimi  37608  bj-eximcom  37609  bj-subst  37653  bj-gabss  37941  wl-mo3t  38602  wl-eujustlem1  38614  pm10.56  45448  2exim  45457