Theorem exlimiiv 1974

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

Syntax hints:   → wi 4  ∃wex 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-ex 1824

This theorem is referenced by:  equid  2059  ax7  2063  ax12v2  2165  19.8a  2166  ax6e  2347  axc11n  2392  sbcom2  2523  axext3  2756  bm1.3ii  5022  inf3  8831  epfrs  8906  kmlem2  9310  axcc2lem  9595  dcomex  9606  axdclem2  9679  grothpw  9985  grothpwex  9986  grothomex  9988  grothac  9989  cnso  15384  aannenlem3  24526  bj-ax6e  33247  wl-spae  33905