Theorem eximii 1625

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

Syntax hints:   -> wi 4   E.wex 1515

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1722  ax6evr  1728  spimed  1763  darii  2154  barbari  2156  festino  2160  baroco  2161  cesaro  2162  camestros  2163  datisi  2164  disamis  2165  felapton  2168  darapti  2169  dimatis  2171  fresison  2172  calemos  2173  fesapo  2174  bamalip  2175  ceqsexv2d  2812  vtoclf  2826  vtocl2  2828  vtocl3  2829  nalset  4175  el  4223  dtruarb  4236  snnex  4496  eusv2nf  4504  dtruex  4608  limom  4663  nninfct  12395  bj-axemptylem  15865  bj-nalset  15868  bj-d0clsepcl  15898  bj-omex2  15950  bj-nn0sucALT  15951