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  2186  19.8a  2188  ax6e  2387  axc11n  2430  vtocle  3512  vtoclOLD  3516  bm1.3iiOLD  5247  axprlem1  5368  axprlem2  5369  axpr  5372  axprOLD  5376  elirrv  9502  inf3  9544  omex  9552  epfrs  9640  kmlem2  10062  axcc2lem  10346  dcomex  10357  axdclem2  10430  pwcfsdom  10494  grothpw  10737  grothpwex  10738  grothomex  10740  grothac  10741  cnso  16172  aannenlem3  26294  mulog2sum  27504  axnulALT2  35265  in-ax8  36418  ss-ax8  36419  regsfromregtr  36668  bj-ax12  36858  bj-ax6e  36869  wl-spae  37726  ormkglobd  47119