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  3514  vtoclOLD  3518  bm1.3iiOLD  5249  axprlem1  5370  axprlem2  5371  axpr  5374  axprOLD  5378  elirrv  9514  inf3  9556  omex  9564  epfrs  9652  kmlem2  10074  axcc2lem  10358  dcomex  10369  axdclem2  10442  pwcfsdom  10506  grothpw  10749  grothpwex  10750  grothomex  10752  grothac  10753  cnso  16184  aannenlem3  26306  mulog2sum  27516  axnulALT3  35286  axprALT2  35287  in-ax8  36440  ss-ax8  36441  regsfromregtr  36690  bj-ax12  36902  bj-ax6e  36913  wl-spae  37776  ormkglobd  47233