Theorem exlimiiv 1929

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  equid  2009  ax7  2013  sbcom2  2171  ax12v2  2177  19.8a  2179  ax6e  2386  axc11n  2429  vtocle  3555  vtoclOLD  3559  bm1.3iiOLD  5308  axprlem1  5429  axprlem2  5430  axpr  5433  axprOLD  5437  inf3  9673  epfrs  9769  kmlem2  10190  axcc2lem  10474  dcomex  10485  axdclem2  10558  grothpw  10864  grothpwex  10865  grothomex  10867  grothac  10868  cnso  16280  aannenlem3  26387  axnulALT2  35086  in-ax8  36207  ss-ax8  36208  bj-ax12  36640  bj-ax6e  36651  wl-spae  37502