Theorem aleximi 1835

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1537  ∃wex 1783

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

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  alexbii  1836  exim  1837  eximdh  1868  19.29  1877  19.29r  1878  19.35  1881  19.25  1884  19.30  1885  19.40b  1892  exintr  1896  19.36imv  1949  speimfw  1968  aeveq  2060  sbequ2  2244  2ax6elem  2470  sb1  2479  dfeumo  2537  mo3  2564  mo4  2566  mopick  2627  2mo  2650  ssel  3910  ssopab2  5452  ssoprab2  7321  axextnd  10278  bj-2exim  34720  bj-exalimi  34741  bj-cbvalimt  34747  bj-eximcom  34751  bj-subst  34769  bj-gabss  35050  wl-mo3t  35658  pm10.56  41877  2exim  41886