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  2217  ax6e  2412  axc11n  2455  vtocle  3518  bm1.3iiOLD  5259  vneqv  5273  axprlem2  5389  axpr  5392  axprlem1OLD  5393  axprOLD  5397  elirrv  9569  elirrvOLD  9570  inf3  9614  omex  9622  epfrs  9710  kmlem2  10154  axcc2lem  10438  dcomex  10449  axdclem2  10522  pwcfsdom  10592  grothpw  10835  grothpwex  10836  grothomex  10838  grothac  10839  cnso  16335  aannenlem3  26566  mulog2sum  27773  axnulALT3  35616  axprALT2  35617  in-ax8  36844  ss-ax8  36845  axtco1from2  37094  axnulregtco  37099  regsfromregtco  37157  mh-inf3sn  37161  bj-ax12  37387  bj-ax6e  37398  wl-spae  38284  ormkglobd  47705