Theorem eximii 1534

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

Syntax hints:   -> wi 4   E.wex 1422

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  spimed  1669  darii  2042  barbari  2044  festino  2048  baroco  2049  cesaro  2050  camestros  2051  datisi  2052  disamis  2053  felapton  2056  darapti  2057  dimatis  2059  fresison  2060  calemos  2061  fesapo  2062  bamalip  2063  vtoclf  2653  vtocl2  2655  vtocl3  2656  nalset  3916  el  3960  dtruarb  3970  snnex  4207  eusv2nf  4214  dtruex  4310  limom  4362  bj-axemptylem  10841  bj-nalset  10844  bj-d0clsepcl  10878  bj-omex2  10930  bj-nn0sucALT  10931