Theorem exlimiiv 1930

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

Syntax hints:   → wi 4  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  equid  2010  ax7  2014  sbcom2  2172  ax12v2  2178  19.8a  2180  ax6e  2387  axc11n  2430  vtocle  3554  vtoclOLD  3558  bm1.3iiOLD  5301  axprlem1  5422  axprlem2  5423  axpr  5426  axprOLD  5430  inf3  9676  omex  9684  epfrs  9772  kmlem2  10193  axcc2lem  10477  dcomex  10488  axdclem2  10561  pwcfsdom  10624  grothpw  10867  grothpwex  10868  grothomex  10870  grothac  10871  cnso  16284  aannenlem3  26373  mulog2sum  27582  axnulALT2  35108  in-ax8  36226  ss-ax8  36227  bj-ax12  36659  bj-ax6e  36670  wl-spae  37523  ormkglobd  46895