Theorem exlimiiv 1932

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  equid  2013  ax7  2017  sbcom2  2178  ax12v2  2184  19.8a  2186  ax6e  2385  axc11n  2428  vtocle  3509  vtoclOLD  3513  bm1.3iiOLD  5244  axprlem1  5365  axprlem2  5366  axpr  5369  axprOLD  5373  elirrv  9494  inf3  9536  omex  9544  epfrs  9632  kmlem2  10054  axcc2lem  10338  dcomex  10349  axdclem2  10422  pwcfsdom  10485  grothpw  10728  grothpwex  10729  grothomex  10731  grothac  10732  cnso  16163  aannenlem3  26285  mulog2sum  27495  axnulALT2  35192  in-ax8  36340  ss-ax8  36341  bj-ax12  36774  bj-ax6e  36785  wl-spae  37638  ormkglobd  47035