Theorem aleximi 1831

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

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

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

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

This theorem is referenced by:  alexbii  1832  exim  1833  eximdh  1863  19.29  1872  19.29r  1873  19.35  1876  19.25  1879  19.30  1880  19.40b  1887  exintr  1891  19.36imv  1944  speimfw  1962  aeveq  2055  sbequ2  2248  2ax6elem  2473  sb1  2481  dfeumo  2535  mo3  2562  mo4  2564  mopick  2623  2mo  2646  ssel  3957  ssrexv  4033  axprlem4  5406  ssopab2  5531  ssoprab2  7483  axextnd  10613  bj-2exim  36571  bj-exalimi  36593  bj-cbvalimt  36599  bj-eximcom  36603  bj-subst  36621  bj-gabss  36895  wl-mo3t  37536  pm10.56  44346  2exim  44355