Theorem exlimiiv 1932

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  equid  2019  ax7  2023  sbcom2  2168  ax12v2  2179  19.8a  2180  ax6e  2401  axc11n  2448  vtocl  3561  bm1.3ii  5208  axprlem1  5326  axprlem2  5327  axpr  5331  inf3  9100  epfrs  9175  kmlem2  9579  axcc2lem  9860  dcomex  9871  axdclem2  9944  grothpw  10250  grothpwex  10251  grothomex  10253  grothac  10254  cnso  15602  aannenlem3  24921  bj-ax12  33992  bj-ax6e  34003  wl-spae  34763