Theorem eximii 1595

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

Syntax hints:   -> wi 4   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spimfv  1692  ax6evr  1698  spimed  1733  darii  2119  barbari  2121  festino  2125  baroco  2126  cesaro  2127  camestros  2128  datisi  2129  disamis  2130  felapton  2133  darapti  2134  dimatis  2136  fresison  2137  calemos  2138  fesapo  2139  bamalip  2140  vtoclf  2783  vtocl2  2785  vtocl3  2786  nalset  4117  el  4162  dtruarb  4175  snnex  4431  eusv2nf  4439  dtruex  4541  limom  4596  bj-axemptylem  13892  bj-nalset  13895  bj-d0clsepcl  13925  bj-omex2  13977  bj-nn0sucALT  13978