Theorem aleximi 1756

Description: A variant of al2imi 1740: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2025, sps 2053 and eximd 2083, 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 148	. . . 4 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	al2imi 1740	. . 3 ⊢ (∀𝑥𝜑 → (∀𝑥 ¬ 𝜒 → ∀𝑥 ¬ 𝜓))
4		alnex 1703	. . 3 ⊢ (∀𝑥 ¬ 𝜒 ↔ ¬ ∃𝑥𝜒)
5		alnex 1703	. . 3 ⊢ (∀𝑥 ¬ 𝜓 ↔ ¬ ∃𝑥𝜓)
6	3, 4, 5	3imtr3g 284	. 2 ⊢ (∀𝑥𝜑 → (¬ ∃𝑥𝜒 → ¬ ∃𝑥𝜓))
7	6	con4d 114	1 ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1478  ∃wex 1701

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

This theorem depends on definitions:  df-bi 197  df-ex 1702

This theorem is referenced by:  alexbii  1757  exim  1758  exanOLD  1786  eximdh  1788  19.29  1798  19.29r  1799  19.35  1802  19.25  1805  19.30  1806  19.40b  1812  speimfw  1873  aeveq  1979  aevOLD  2159  2ax6elem  2448  mo3  2506  mopick  2534  2mo  2550  ssopab2  4961  ssoprab2  6664  axextnd  9357  bj-2exim  32237  bj-exalimi  32254  bj-sb56  32281  wl-dveeq12  32943  wl-mo3t  32990  pm10.56  38051  2exim  38060