Theorem exlimiiv 1964

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  equid  2045  ax7  2049  sbcom2  2210  ax12v2  2218  19.8a  2220  ax6e  2417  axc11n  2460  vtocle  3525  bm1.3iiOLD  5267  vneqv  5281  axprlem2  5397  axpr  5400  axprlem1OLD  5401  axprOLD  5405  elirrv  9566  elirrvOLD  9567  inf3  9611  omex  9619  epfrs  9707  kmlem2  10151  axcc2lem  10435  dcomex  10446  axdclem2  10519  pwcfsdom  10583  grothpw  10826  grothpwex  10827  grothomex  10829  grothac  10830  cnso  16325  aannenlem3  26544  mulog2sum  27752  axnulALT3  35560  axprALT2  35561  in-ax8  36793  ss-ax8  36794  axtco1from2  37043  axnulregtco  37048  regsfromregtco  37106  mh-inf3sn  37110  bj-ax12  37336  bj-ax6e  37347  wl-spae  38233  ormkglobd  47649