Theorem exlimiiv 1846

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

Syntax hints:   → wi 4  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  equid  1926  ax7  1930  ax12v2  2036  ax12vOLD  2037  ax12vOLDOLD  2038  19.8a  2039  ax6e  2238  axc11n  2295  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  axext3  2592  bm1.3ii  4712  inf3  8415  epfrs  8490  kmlem2  8856  axcc2lem  9141  dcomex  9152  axdclem2  9225  grothpw  9527  grothpwex  9528  grothomex  9530  grothac  9531  cnso  14815  aannenlem3  23889  bj-ax6e  31842  wl-spae  32485