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  3521  vtoclOLD  3525  bm1.3iiOLD  5257  axprlem1  5378  axprlem2  5379  axpr  5382  axprOLD  5386  inf3  9588  omex  9596  epfrs  9684  kmlem2  10105  axcc2lem  10389  dcomex  10400  axdclem2  10473  pwcfsdom  10536  grothpw  10779  grothpwex  10780  grothomex  10782  grothac  10783  cnso  16215  aannenlem3  26238  mulog2sum  27448  axnulALT2  35083  in-ax8  36212  ss-ax8  36213  bj-ax12  36645  bj-ax6e  36656  wl-spae  37509  ormkglobd  46873