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  2215  19.8a  2218  ax6e  2413  axc11n  2456  vtocle  3519  vneqv  5270  axprlem2  5386  axpr  5389  axprlem1OLD  5390  elirrv  9584  elirrvOLD  9585  inf3  9629  omex  9637  epfrs  9725  kmlem2  10223  axcc2lem  10507  dcomex  10518  axdclem2  10591  pwcfsdom  10661  grothpw  10904  grothpwex  10905  grothomex  10907  grothac  10908  cnso  16408  aannenlem3  26650  mulog2sum  27857  axnulALT3  35722  axprALT2  35723  in-ax8  36993  ss-ax8  36994  axtco1from2  37243  axnulregtco  37248  regsfromregtco  37306  mh-inf3sn  37310  bj-ax12  37536  bj-ax6e  37547  wl-spae  38433  ormkglobd  47856