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 2156, sps 2190 and eximd 2221, 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  2254  2ax6elem  2472  sb1  2480  dfeumo  2534  mo3  2561  mo4  2563  mopick  2622  2mo  2645  ssel  3924  ssrexv  4000  axprlem4  5366  ssopab2  5489  ssoprab2  7420  axextnd  10489  bj-2exim  36676  bj-exalimi  36698  bj-cbvalimt  36704  bj-eximcom  36708  bj-subst  36726  bj-gabss  37000  wl-mo3t  37641  pm10.56  44487  2exim  44496