Theorem aleximi 1833

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539  ∃wex 1780

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

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

This theorem is referenced by:  alexbii  1834  exim  1835  eximdh  1865  19.29  1874  19.29r  1875  19.35  1878  19.25  1881  19.30  1882  19.40b  1889  exintr  1893  19.36imv  1946  speimfw  1964  aeveq  2059  sbequ2  2256  2ax6elem  2474  sb1  2482  dfeumo  2536  mo3  2564  mo4  2566  mopick  2625  2mo  2648  ssel  3927  ssrexv  4003  axprlem4  5371  ssopab2  5494  ssoprab2  7426  axextnd  10502  bj-2exim  36811  bj-exalimi  36833  bj-cbvalimt  36839  bj-eximcom  36843  bj-subst  36862  bj-gabss  37136  wl-mo3t  37777  wl-eujustlem1  37789  pm10.56  44607  2exim  44616