Theorem eximii 1490

Description: Inference associated with eximi 1488. (Contributed by BJ, 3-Feb-2018.)

Hypotheses

Ref	Expression
eximii.1	|- E.xph
eximii.2	|- (ph -> ps)

Assertion

Ref	Expression
eximii	|- E.xps

Proof of Theorem eximii

Step	Hyp	Ref	Expression
1		eximii.1	. 2 |- E.xph
2		eximii.2	. . 3 |- (ph -> ps)
3	2	eximi 1488	. 2 |- (E.xph -> E.xps)
4	1, 3	ax-mp 7	1 |- E.xps

Syntax hints:   -> wi 4  E.wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  spimed  1625  darii  1997  barbari  1999  festino  2003  baroco  2004  cesaro  2005  camestros  2006  datisi  2007  disamis  2008  felapton  2011  darapti  2012  dimatis  2014  fresison  2015  calemos  2016  fesapo  2017  bamalip  2018  vtoclf  2601  vtocl2  2603  vtocl3  2604  nalset  3878  el  3922  dtruarb  3933  snnex  4147  eusv2nf  4154  limom  4279  bj-axemptylem  9347  bj-nalset  9350  bj-d0clsepcl  9384  bj-omex2  9437  bj-nn0sucALT  9438