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 1783

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

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

This theorem is referenced by:  equid  2016  ax7  2020  sbcom2  2163  ax12v2  2175  19.8a  2176  ax6e  2383  axc11n  2426  vtocl  3488  bm1.3ii  5221  axprlem1  5341  axprlem2  5342  axpr  5346  inf3  9323  epfrs  9420  kmlem2  9838  axcc2lem  10123  dcomex  10134  axdclem2  10207  grothpw  10513  grothpwex  10514  grothomex  10516  grothac  10517  cnso  15884  aannenlem3  25395  bj-ax12  34765  bj-ax6e  34776  wl-spae  35607