Theorem exlimiiv 1859

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

Syntax hints:   → wi 4  ∃wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  equid  1939  ax7  1943  ax12v2  2049  ax12vOLD  2050  ax12vOLDOLD  2051  19.8a  2052  ax6e  2250  axc11n  2307  axc11nOLD  2308  axc11nOLDOLD  2309  axc11nALT  2310  axext3  2604  bm1.3ii  4784  inf3  8532  epfrs  8607  kmlem2  8973  axcc2lem  9258  dcomex  9269  axdclem2  9342  grothpw  9648  grothpwex  9649  grothomex  9651  grothac  9652  cnso  14976  aannenlem3  24085  bj-ax6e  32653  wl-spae  33306