Theorem exlimiiv 1933

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  equid  2014  ax7  2018  sbcom2  2179  ax12v2  2187  19.8a  2189  ax6e  2388  axc11n  2431  vtocle  3501  vtoclOLD  3505  bm1.3iiOLD  5237  axprlem2  5361  axpr  5364  axprlem1OLD  5365  axprOLD  5369  elirrv  9505  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  26307  mulog2sum  27514  axnulALT3  35268  axprALT2  35269  in-ax8  36422  ss-ax8  36423  axtco1from2  36673  axnulregtco  36678  regsfromregtco  36736  mh-inf3sn  36740  bj-ax12  36967  bj-ax6e  36978  wl-spae  37860  ormkglobd  47321