Theorem aleximi 1839

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  alexbii  1840  exim  1841  eximdh  1871  19.29  1880  19.29r  1881  19.35  1884  19.25  1887  19.30  1888  19.40b  1895  exintr  1899  19.36imv  1952  speimfw  1970  aeveq  2065  sbequ2  2261  2ax6elem  2478  sb1  2486  dfeumo  2540  mo3  2568  mo4  2570  mopick  2629  2mo  2652  ssel  3916  ssrexv  3991  axprlem4  5362  ssopab2  5495  ssoprab2  7431  elirrv  9509  axextnd  10512  axnulregtco  36715  bj-2exim  36948  bj-exalimi  36963  bj-eximcom  36964  bj-subst  37008  bj-gabss  37295  wl-mo3t  37954  wl-eujustlem1  37966  pm10.56  44821  2exim  44830