Theorem aleximi 1749

Description: A variant of al2imi 1733: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2015, sps 2043 and eximd 2072, 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 147	. . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	al2imi 1733	. . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4		alnex 1697	. . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5		alnex 1697	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
6	3, 4, 5	3imtr3g 283	. 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
7	6	con4d 113	1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1473  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  alexbii  1750  exim  1751  exbiOLD  1763  exanOLD  1776  eximdh  1778  19.29  1789  19.29r  1790  19.35  1794  19.25  1797  19.30  1798  19.40b  1804  speimfw  1863  aeveq  1969  aevOLD  2148  2ax6elem  2437  mo3  2495  mopick  2523  2mo  2539  eleq2dOLD  2674  ssopab2  4926  ssoprab2  6609  axextnd  9292  bj-2exim  31780  bj-exaleximi  31800  bj-sb56  31828  wl-dveeq12  32490  wl-mo3t  32537  pm10.56  37591  2exim  37600