Theorem exlimiiv 1931

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  equid  2012  ax7  2016  sbcom2  2174  ax12v2  2180  19.8a  2182  ax6e  2381  axc11n  2424  vtocle  3510  vtoclOLD  3514  bm1.3iiOLD  5241  axprlem1  5362  axprlem2  5363  axpr  5366  axprOLD  5370  elirrv  9489  inf3  9531  omex  9539  epfrs  9627  kmlem2  10046  axcc2lem  10330  dcomex  10341  axdclem2  10414  pwcfsdom  10477  grothpw  10720  grothpwex  10721  grothomex  10723  grothac  10724  cnso  16156  aannenlem3  26236  mulog2sum  27446  axnulALT2  35060  in-ax8  36198  ss-ax8  36199  bj-ax12  36631  bj-ax6e  36642  wl-spae  37495  ormkglobd  46856