Theorem aleximi 1828

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1531  ∃wex 1776

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

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  alexbii  1829  exim  1830  eximdh  1861  19.29  1870  19.29r  1871  19.35  1874  19.25  1877  19.30  1878  19.40b  1885  exintr  1889  speimfw  1962  aeveq  2057  sbequ2  2246  2ax6elem  2489  sb1  2499  dfeumo  2615  mo3  2644  mo4  2646  mopick  2706  2mo  2729  ssopab2  5425  ssoprab2  7216  axextnd  10007  bj-2exim  33940  bj-exalimi  33961  bj-cbvalimt  33967  bj-eximcom  33971  bj-sb56  33989  wl-mo3t  34806  pm10.56  40695  2exim  40704