Theorem aleximi 1834

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540  ∃wex 1781

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

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

This theorem is referenced by:  alexbii  1835  exim  1836  eximdh  1866  19.29  1875  19.29r  1876  19.35  1879  19.25  1882  19.30  1883  19.40b  1890  exintr  1894  19.36imv  1947  speimfw  1965  aeveq  2060  sbequ2  2257  2ax6elem  2475  sb1  2483  dfeumo  2537  mo3  2565  mo4  2567  mopick  2626  2mo  2649  ssel  3916  ssrexv  3992  axprlem4  5363  ssopab2  5494  ssoprab2  7428  axextnd  10505  axnulregtco  36678  bj-2exim  36911  bj-exalimi  36926  bj-eximcom  36927  bj-subst  36971  bj-gabss  37258  wl-mo3t  37915  wl-eujustlem1  37927  pm10.56  44815  2exim  44824