Theorem exlimiiv 1963

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  equid  2044  ax7  2048  sbcom2  2208  ax12v2  2214  19.8a  2217  ax6e  2412  axc11n  2455  vtocle  3518  vneqv  5269  axprlem2  5386  axpr  5389  axprlem1OLD  5390  elirrv  9598  elirrvOLD  9599  inf3  9643  omex  9651  epfrs  9739  kmlem2  10237  axcc2lem  10521  dcomex  10532  axdclem2  10605  pwcfsdom  10675  grothpw  10918  grothpwex  10919  grothomex  10921  grothac  10922  cnso  16424  aannenlem3  26666  mulog2sum  27873  axnulALT3  35789  axprALT2  35790  in-ax8  37109  ss-ax8  37110  axtco1from2  37359  axnulregtco  37364  regsfromregtco  37422  mh-inf3sn  37426  bj-ax12  37652  bj-ax6e  37663  wl-spae  38562  ormkglobd  47995