Theorem exlimiiv 1961

Description: Inference (Rule C) associated with exlimiv 1960. (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 1960	. 2 ⊢ (∃𝑥𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  equid  2042  ax7  2046  sbcom2  2207  ax12v2  2215  19.8a  2217  ax6e  2415  axc11n  2458  vtocle  3523  bm1.3iiOLD  5265  vneqv  5279  axprlem2  5395  axpr  5398  axprlem1OLD  5399  axprOLD  5403  elirrv  9555  elirrvOLD  9556  inf3  9600  omex  9608  epfrs  9696  kmlem2  10131  axcc2lem  10415  dcomex  10426  axdclem2  10499  pwcfsdom  10563  grothpw  10806  grothpwex  10807  grothomex  10809  grothac  10810  cnso  16298  aannenlem3  26493  mulog2sum  27701  axnulALT3  35502  axprALT2  35503  in-ax8  36736  ss-ax8  36737  axtco1from2  36986  axnulregtco  36991  regsfromregtco  37049  mh-inf3sn  37053  bj-ax12  37279  bj-ax6e  37290  wl-spae  38176  ormkglobd  47591