Theorem eximii 1616

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

Syntax hints:   -> wi 4   E.wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1713  ax6evr  1719  spimed  1754  darii  2145  barbari  2147  festino  2151  baroco  2152  cesaro  2153  camestros  2154  datisi  2155  disamis  2156  felapton  2159  darapti  2160  dimatis  2162  fresison  2163  calemos  2164  fesapo  2165  bamalip  2166  ceqsexv2d  2803  vtoclf  2817  vtocl2  2819  vtocl3  2820  nalset  4163  el  4211  dtruarb  4224  snnex  4483  eusv2nf  4491  dtruex  4595  limom  4650  nninfct  12208  bj-axemptylem  15538  bj-nalset  15541  bj-d0clsepcl  15571  bj-omex2  15623  bj-nn0sucALT  15624