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  2474  sb1  2482  dfeumo  2536  mo3  2564  mo4  2566  mopick  2625  2mo  2648  ssel  3915  ssrexv  3991  axprlem4  5368  ssopab2  5501  ssoprab2  7435  axextnd  10514  axnulregtco  36662  bj-2exim  36895  bj-exalimi  36910  bj-eximcom  36911  bj-subst  36955  bj-gabss  37242  wl-mo3t  37901  wl-eujustlem1  37913  pm10.56  44797  2exim  44806