Theorem exlimiiv 1926

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

Syntax hints:   → wi 4  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

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

This theorem is referenced by:  equid  2007  ax7  2011  sbcom2  2153  ax12v2  2165  19.8a  2166  ax6e  2376  axc11n  2419  vtocl  3540  bm1.3ii  5295  axprlem1  5414  axprlem2  5415  axpr  5419  inf3  9632  epfrs  9728  kmlem2  10148  axcc2lem  10433  dcomex  10444  axdclem2  10517  grothpw  10823  grothpwex  10824  grothomex  10826  grothac  10827  cnso  16197  aannenlem3  26220  bj-ax12  36042  bj-ax6e  36053  wl-spae  36897