Theorem eximii 1582

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

Syntax hints:   -> wi 4   E.wex 1469

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1682  spimed  1719  darii  2100  barbari  2102  festino  2106  baroco  2107  cesaro  2108  camestros  2109  datisi  2110  disamis  2111  felapton  2114  darapti  2115  dimatis  2117  fresison  2118  calemos  2119  fesapo  2120  bamalip  2121  vtoclf  2742  vtocl2  2744  vtocl3  2745  nalset  4066  el  4110  dtruarb  4123  snnex  4377  eusv2nf  4385  dtruex  4482  limom  4535  bj-axemptylem  13261  bj-nalset  13264  bj-d0clsepcl  13294  bj-omex2  13346  bj-nn0sucALT  13347