Theorem exlimiiv 1951

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

Syntax hints:   → wi 4  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  equid  2032  ax7  2036  sbcom2  2206  ax12v2  2214  19.8a  2216  ax6e  2414  axc11n  2457  vtocle  3523  bm1.3iiOLD  5252  vneqv  5266  axprlem2  5381  axpr  5384  axprlem1OLD  5385  axprOLD  5389  elirrv  9545  elirrvOLD  9546  inf3  9590  omex  9598  epfrs  9686  kmlem2  10108  axcc2lem  10393  dcomex  10404  axdclem2  10477  pwcfsdom  10541  grothpw  10784  grothpwex  10785  grothomex  10787  grothac  10788  cnso  16279  aannenlem3  26391  mulog2sum  27598  axnulALT3  35401  axprALT2  35402  in-ax8  36581  ss-ax8  36582  axtco1from2  36832  axnulregtco  36837  regsfromregtco  36895  mh-inf3sn  36899  bj-ax12  37126  bj-ax6e  37137  wl-spae  38021  ormkglobd  47448