Theorem exlimiiv 1966

Description: Inference (Rule C) associated with exlimiv 1965. (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 1965	. 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 1945

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

This theorem is used by:  equid  2047  ax7  2051  sbcom2  2212  ax12v2  2218  19.8a  2221  ax6e  2415  axc11n  2458  vtocle  3522  vneqv  5276  axprlem2  5393  axpr  5396  axprlem1OLD  5397  elirrv  9628  elirrvOLD  9629  inf3  9673  omex  9681  epfrs  9769  kmlem2  10269  axcc2lem  10553  dcomex  10564  axdclem2  10637  pwcfsdom  10707  grothpw  10950  grothpwex  10951  grothomex  10953  grothac  10954  cnso  16459  aannenlem3  26714  mulog2sum  27921  axnulALT3  35856  axprALT2  35857  in-ax8  37228  ss-ax8  37229  axtco1from2  37478  axnulregtco  37483  regsfromregtco  37541  mh-inf3sn  37545  bj-ax12  37771  bj-ax6e  37782  wl-spae  38721  ormkglobd  48160