Theorem exlimiiv 1935

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  equid  2016  ax7  2020  sbcom2  2162  ax12v2  2174  19.8a  2175  ax6e  2383  axc11n  2426  vtocl  3550  bm1.3ii  5303  axprlem1  5422  axprlem2  5423  axpr  5427  inf3  9630  epfrs  9726  kmlem2  10146  axcc2lem  10431  dcomex  10442  axdclem2  10515  grothpw  10821  grothpwex  10822  grothomex  10824  grothac  10825  cnso  16190  aannenlem3  25843  bj-ax12  35534  bj-ax6e  35545  wl-spae  36390