Theorem exlimiiv 1958

Description: Inference (Rule C) associated with exlimiv 1957. (Contributed by BJ, 19-Dec-2020.)

Hypotheses

Ref	Expression
exlimiv.1	⊢ (𝜑 → 𝜓)
exlimiiv.2	⊢ ∃𝑥𝜑

Assertion

Ref	Expression
exlimiiv	⊢ 𝜓

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiiv

Step	Hyp	Ref	Expression
1		exlimiiv.2	. 2 ⊢ ∃𝑥𝜑
2		exlimiv.1	. . 3 ⊢ (𝜑 → 𝜓)
3	2	exlimiv 1957	. 2 ⊢ (∃𝑥𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  equid  2039  ax7  2043  sbcom2  2213  ax12v2  2221  19.8a  2223  ax6e  2421  axc11n  2464  vtocle  3532  bm1.3iiOLD  5267  vneqv  5281  axprlem2  5396  axpr  5399  axprlem1OLD  5400  axprOLD  5404  elirrv  9558  elirrvOLD  9559  inf3  9603  omex  9611  epfrs  9699  kmlem2  10134  axcc2lem  10419  dcomex  10430  axdclem2  10503  pwcfsdom  10567  grothpw  10810  grothpwex  10811  grothomex  10813  grothac  10814  cnso  16302  aannenlem3  26459  mulog2sum  27666  axnulALT3  35443  axprALT2  35444  in-ax8  36624  ss-ax8  36625  axtco1from2  36874  axnulregtco  36879  regsfromregtco  36937  mh-inf3sn  36941  bj-ax12  37167  bj-ax6e  37178  wl-spae  38063  ormkglobd  47482