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 2154, sps 2188 and eximd 2219, 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  2252  2ax6elem  2470  sb1  2478  dfeumo  2532  mo3  2559  mo4  2561  mopick  2620  2mo  2643  ssel  3928  ssrexv  4004  axprlem4  5364  ssopab2  5486  ssoprab2  7414  axextnd  10479  bj-2exim  36644  bj-exalimi  36666  bj-cbvalimt  36672  bj-eximcom  36676  bj-subst  36694  bj-gabss  36968  wl-mo3t  37609  pm10.56  44402  2exim  44411