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 1777

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

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

This theorem is referenced by:  equid  2011  ax7  2015  sbcom2  2174  ax12v2  2180  19.8a  2182  ax6e  2391  axc11n  2434  vtocle  3567  vtoclOLD  3571  bm1.3ii  5320  axprlem1  5441  axprlem2  5442  axpr  5446  inf3  9704  epfrs  9800  kmlem2  10221  axcc2lem  10505  dcomex  10516  axdclem2  10589  grothpw  10895  grothpwex  10896  grothomex  10898  grothac  10899  cnso  16295  aannenlem3  26390  axnulALT2  35069  in-ax8  36190  ss-ax8  36191  bj-ax12  36623  bj-ax6e  36634  wl-spae  37475