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 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 1913

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

This theorem is referenced by:  equid  2015  ax7  2019  sbcom2  2161  ax12v2  2173  19.8a  2174  ax6e  2383  axc11n  2426  vtocl  3498  bm1.3ii  5226  axprlem1  5346  axprlem2  5347  axpr  5351  inf3  9393  epfrs  9489  kmlem2  9907  axcc2lem  10192  dcomex  10203  axdclem2  10276  grothpw  10582  grothpwex  10583  grothomex  10585  grothac  10586  cnso  15956  aannenlem3  25490  bj-ax12  34838  bj-ax6e  34849  wl-spae  35680