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  2176  ax12v2  2182  19.8a  2184  ax6e  2383  axc11n  2426  vtocle  3508  vtoclOLD  3512  bm1.3iiOLD  5235  axprlem1  5356  axprlem2  5357  axpr  5360  axprOLD  5364  elirrv  9478  inf3  9520  omex  9528  epfrs  9616  kmlem2  10038  axcc2lem  10322  dcomex  10333  axdclem2  10406  pwcfsdom  10469  grothpw  10712  grothpwex  10713  grothomex  10715  grothac  10716  cnso  16151  aannenlem3  26260  mulog2sum  27470  axnulALT2  35112  in-ax8  36258  ss-ax8  36259  bj-ax12  36691  bj-ax6e  36702  wl-spae  37555  ormkglobd  46913