Theorem aleximi 1830

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1535  ∃wex 1777

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

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

This theorem is referenced by:  alexbii  1831  exim  1832  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  1963  aeveq  2056  sbequ2  2250  2ax6elem  2478  sb1  2486  dfeumo  2540  mo3  2567  mo4  2569  mopick  2628  2mo  2651  ssel  4002  ssrexv  4078  ssopab2  5565  ssoprab2  7518  axextnd  10660  bj-2exim  36577  bj-exalimi  36599  bj-cbvalimt  36605  bj-eximcom  36609  bj-subst  36627  bj-gabss  36901  wl-mo3t  37530  pm10.56  44339  2exim  44348