Theorem exlimiiv 1996

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

Syntax hints:   → wi 4  ∃wex 1841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976

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

This theorem is referenced by:  equid  2082  ax7  2086  ax12v2  2186  19.8a  2187  ax6e  2383  axc11n  2439  axc11nOLD  2440  axext3  2730  bm1.3ii  4924  inf3  8693  epfrs  8768  kmlem2  9136  axcc2lem  9421  dcomex  9432  axdclem2  9505  grothpw  9811  grothpwex  9812  grothomex  9814  grothac  9815  cnso  15146  aannenlem3  24255  bj-ax6e  32930  wl-spae  33588