Theorem exlimiiv 1934

Description: Inference (Rule C) associated with exlimiv 1933. (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 1933	. 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 1913

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

This theorem is referenced by:  equid  2015  ax7  2019  sbcom2  2161  ax12v2  2173  19.8a  2174  ax6e  2381  axc11n  2424  vtocl  3519  bm1.3ii  5264  axprlem1  5383  axprlem2  5384  axpr  5388  inf3  9580  epfrs  9676  kmlem2  10096  axcc2lem  10381  dcomex  10392  axdclem2  10465  grothpw  10771  grothpwex  10772  grothomex  10774  grothac  10775  cnso  16140  aannenlem3  25727  bj-ax12  35197  bj-ax6e  35208  wl-spae  36053