Theorem exlimiiv 1938

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

Syntax hints:   → wi 4  ∃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  ax-5 1917

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

This theorem is referenced by:  equid  2019  ax7  2023  sbcom2  2183  ax12v2  2191  19.8a  2193  ax6e  2391  axc11n  2434  vtocle  3501  vtoclOLD  3504  bm1.3iiOLD  5224  vneqv  5238  axprlem2  5353  axpr  5356  axprlem1OLD  5357  axprOLD  5361  elirrv  9502  elirrvOLD  9503  inf3  9547  omex  9555  epfrs  9643  kmlem2  10065  axcc2lem  10349  dcomex  10360  axdclem2  10433  pwcfsdom  10497  grothpw  10740  grothpwex  10741  grothomex  10743  grothac  10744  cnso  16205  aannenlem3  26314  mulog2sum  27518  axnulALT3  35289  axprALT2  35290  in-ax8  36452  ss-ax8  36453  axtco1from2  36703  axnulregtco  36708  regsfromregtco  36766  mh-inf3sn  36770  bj-ax12  36997  bj-ax6e  37008  wl-spae  37892  ormkglobd  47320