Theorem eximii 1602

Description: Inference associated with eximi 1600. (Contributed by BJ, 3-Feb-2018.)

Hypotheses

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

Assertion

Ref	Expression
eximii	|- E. x ps

Proof of Theorem eximii

Step	Hyp	Ref	Expression
1		eximii.1	. 2 |- E. x ph
2		eximii.2	. . 3 |- ( ph -> ps )
3	2	eximi 1600	. 2 |- ( E. x ph -> E. x ps )
4	1, 3	ax-mp 5	1 |- E. x ps

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1699  ax6evr  1705  spimed  1740  darii  2126  barbari  2128  festino  2132  baroco  2133  cesaro  2134  camestros  2135  datisi  2136  disamis  2137  felapton  2140  darapti  2141  dimatis  2143  fresison  2144  calemos  2145  fesapo  2146  bamalip  2147  vtoclf  2791  vtocl2  2793  vtocl3  2794  nalset  4134  el  4179  dtruarb  4192  snnex  4449  eusv2nf  4457  dtruex  4559  limom  4614  bj-axemptylem  14647  bj-nalset  14650  bj-d0clsepcl  14680  bj-omex2  14732  bj-nn0sucALT  14733