Theorem exlimiiv 1785

Description: Inference associated with exlimiv 1784. (Contributed by BJ, 19-Dec-2020.)

Hypotheses

Ref	Expression
exlimiv.1	|- ( ph -> ps )
exlimiiv.2	|- E. x ph

Assertion

Ref	Expression
exlimiiv	|- ps

Distinct variable group:   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem exlimiiv

Step	Hyp	Ref	Expression
1		exlimiiv.2	. 2 |- E. x ph
2		exlimiv.1	. . 3 |- ( ph -> ps )
3	2	exlimiv 1784	. 2 |- ( E. x ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

Syntax hints:   -> wi 4   E.wex 1671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  equid  1863  ax7  1868  ax12v2  1952  ax12vOLD  1953  ax12vOLDOLD  1954  19.8a  1955  ax6e  2107  axc11n  2157  axc11nOLD  2158  axc11nALT  2159  axext3  2453  bm1.3ii  4521  inf3  8158  epfrs  8233  kmlem2  8599  axcc2lem  8884  dcomex  8895  axdclem2  8968  grothpw  9269  grothpwex  9270  grothomex  9272  grothac  9273  cnso  14376  aannenlem3  23365  bj-ax6e  31330  bj-axc11nv  31414