Theorem eximii 1581

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

Syntax hints:   -> wi 4   E.wex 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1681  spimed  1718  darii  2097  barbari  2099  festino  2103  baroco  2104  cesaro  2105  camestros  2106  datisi  2107  disamis  2108  felapton  2111  darapti  2112  dimatis  2114  fresison  2115  calemos  2116  fesapo  2117  bamalip  2118  vtoclf  2734  vtocl2  2736  vtocl3  2737  nalset  4053  el  4097  dtruarb  4110  snnex  4364  eusv2nf  4372  dtruex  4469  limom  4522  bj-axemptylem  13079  bj-nalset  13082  bj-d0clsepcl  13112  bj-omex2  13164  bj-nn0sucALT  13165