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  3546  bm1.3ii  5295  axprlem1  5414  axprlem2  5415  axpr  5419  inf3  9612  epfrs  9708  kmlem2  10128  axcc2lem  10413  dcomex  10424  axdclem2  10497  grothpw  10803  grothpwex  10804  grothomex  10806  grothac  10807  cnso  16172  aannenlem3  25772  bj-ax12  35336  bj-ax6e  35347  wl-spae  36192