Theorem eximii 1536

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

Syntax hints:   -> wi 4   E.wex 1424

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-ial 1470

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax6evr  1636  spimed  1672  darii  2045  barbari  2047  festino  2051  baroco  2052  cesaro  2053  camestros  2054  datisi  2055  disamis  2056  felapton  2059  darapti  2060  dimatis  2062  fresison  2063  calemos  2064  fesapo  2065  bamalip  2066  vtoclf  2666  vtocl2  2668  vtocl3  2669  nalset  3943  el  3987  dtruarb  3999  snnex  4244  eusv2nf  4251  dtruex  4347  limom  4400  bj-axemptylem  11213  bj-nalset  11216  bj-d0clsepcl  11250  bj-omex2  11302  bj-nn0sucALT  11303