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  2209  ax12v2  2217  19.8a  2219  ax6e  2414  axc11n  2457  vtocle  3521  bm1.3iiOLD  5263  vneqv  5277  axprlem2  5393  axpr  5396  axprlem1OLD  5397  axprOLD  5401  elirrv  9572  elirrvOLD  9573  inf3  9617  omex  9625  epfrs  9713  kmlem2  10157  axcc2lem  10441  dcomex  10452  axdclem2  10525  pwcfsdom  10595  grothpw  10838  grothpwex  10839  grothomex  10841  grothac  10842  cnso  16339  aannenlem3  26563  mulog2sum  27771  axnulALT3  35603  axprALT2  35604  in-ax8  36831  ss-ax8  36832  axtco1from2  37081  axnulregtco  37086  regsfromregtco  37144  mh-inf3sn  37148  bj-ax12  37374  bj-ax6e  37385  wl-spae  38271  ormkglobd  47692