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 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  equid  2019  ax7  2023  sbcom2  2165  ax12v2  2177  19.8a  2178  ax6e  2390  axc11n  2437  vtocl  3507  bm1.3ii  5170  axprlem1  5289  axprlem2  5290  axpr  5294  inf3  9082  epfrs  9157  kmlem2  9562  axcc2lem  9847  dcomex  9858  axdclem2  9931  grothpw  10237  grothpwex  10238  grothomex  10240  grothac  10241  cnso  15592  aannenlem3  24926  bj-ax12  34103  bj-ax6e  34114  wl-spae  34926