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  3518  vtoclOLD  3522  bm1.3iiOLD  5252  axprlem1  5373  axprlem2  5374  axpr  5377  axprOLD  5381  inf3  9564  omex  9572  epfrs  9660  kmlem2  10081  axcc2lem  10365  dcomex  10376  axdclem2  10449  pwcfsdom  10512  grothpw  10755  grothpwex  10756  grothomex  10758  grothac  10759  cnso  16191  aannenlem3  26214  mulog2sum  27424  axnulALT2  35056  in-ax8  36185  ss-ax8  36186  bj-ax12  36618  bj-ax6e  36629  wl-spae  37482  ormkglobd  46846