Theorem exlimiiv 1856

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

Syntax hints:   → wi 4  ∃wex 1701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836

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

This theorem is referenced by:  equid  1936  ax7  1940  ax12v2  2046  ax12vOLD  2047  ax12vOLDOLD  2048  19.8a  2049  ax6e  2249  axc11n  2306  axc11nOLD  2307  axc11nOLDOLD  2308  axc11nALT  2309  axext3  2603  bm1.3ii  4754  inf3  8492  epfrs  8567  kmlem2  8933  axcc2lem  9218  dcomex  9229  axdclem2  9302  grothpw  9608  grothpwex  9609  grothomex  9611  grothac  9612  cnso  14920  aannenlem3  24023  bj-ax6e  32348  wl-spae  32977