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  3929  ssrexv  4005  axprlem4  5373  ssopab2  5502  ssoprab2  7436  axextnd  10514  bj-2exim  36843  bj-exalimi  36862  bj-cbvalimt  36869  bj-eximcom  36871  bj-subst  36900  bj-gabss  37177  wl-mo3t  37825  wl-eujustlem1  37837  pm10.56  44720  2exim  44729