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  2162  ax12v2  2168  19.8a  2169  ax6e  2377  axc11n  2420  vtocl  3545  bm1.3ii  5306  axprlem1  5427  axprlem2  5428  axpr  5432  inf3  9668  epfrs  9764  kmlem2  10184  axcc2lem  10469  dcomex  10480  axdclem2  10553  grothpw  10859  grothpwex  10860  grothomex  10862  grothac  10863  cnso  16233  aannenlem3  26293  bj-ax12  36174  bj-ax6e  36185  wl-spae  37029