Theorem exlimiiv 1933

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  equid  2014  ax7  2018  sbcom2  2179  ax12v2  2187  19.8a  2189  ax6e  2387  axc11n  2430  vtocle  3500  vtoclOLD  3504  bm1.3iiOLD  5237  vneqv  5251  axprlem2  5366  axpr  5369  axprlem1OLD  5370  axprOLD  5374  elirrv  9512  inf3  9556  omex  9564  epfrs  9652  kmlem2  10074  axcc2lem  10358  dcomex  10369  axdclem2  10442  pwcfsdom  10506  grothpw  10749  grothpwex  10750  grothomex  10752  grothac  10753  cnso  16214  aannenlem3  26296  mulog2sum  27500  axnulALT3  35252  axprALT2  35253  in-ax8  36406  ss-ax8  36407  axtco1from2  36657  axnulregtco  36662  regsfromregtco  36720  mh-inf3sn  36724  bj-ax12  36951  bj-ax6e  36962  wl-spae  37846  ormkglobd  47305