Theorem eximii 1655

Description: Inference associated with eximi 1653. (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 1653	. 2 |- ( E. x ph -> E. x ps )
4	1, 3	ax-mp 5	1 |- E. x ps

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  spimfv  1751  ax6evr  1757  spimed  1793  darii  2187  barbari  2189  festino  2193  baroco  2194  cesaro  2195  camestros  2196  datisi  2197  disamis  2198  felapton  2201  darapti  2202  dimatis  2204  fresison  2205  calemos  2206  fesapo  2207  bamalip  2208  ceqsexv2d  2862  vtoclf  2876  vtocl2  2878  vtocl3  2879  nalset  4265  el  4317  dtruarb  4330  uniex2  4583  snnex  4596  eusv2nf  4604  dtruex  4708  limom  4763  nninfct  12843  bj-axemptylem  17123  bj-nalset  17126  bj-d0clsepcl  17156  bj-omex2  17208  bj-nn0sucALT  17209