MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eximii Structured version   Visualization version   Unicode version

Theorem eximii 1717
Description: Inference associated with eximi 1715. (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
StepHypRef Expression
1 eximii.1 . 2  |-  E. x ph
2 eximii.2 . . 3  |-  ( ph  ->  ps )
32eximi 1715 . 2  |-  ( E. x ph  ->  E. x ps )
41, 3ax-mp 5 1  |-  E. x ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  exiftru  1816  spimeh  1849  equidOLD  1864  ax6evr  1867  spimv1  2077  cbv3hvOLD  2081  cbv3hvOLDOLD  2082  ax6e  2107  spim  2111  spimed  2112  spimv  2114  spei  2118  equvini  2195  equveli  2196  euequ1  2325  euex  2343  darii  2414  barbari  2416  festino  2420  baroco  2421  cesaro  2422  camestros  2423  datisi  2424  disamis  2425  felapton  2428  darapti  2429  dimatis  2431  fresison  2432  calemos  2433  fesapo  2434  bamalip  2435  vtoclf  3085  vtocl  3086  axrep2  4510  axnul  4525  nalset  4533  notzfaus  4576  el  4583  dtru  4592  eusv2nf  4599  dvdemo1  4635  dvdemo2  4636  axpr  4638  snnex  6616  inf1  8145  bnd  8381  axpowndlem2  9041  grothomex  9272  bnj101  29601  axextdfeq  30515  ax8dfeq  30516  axextndbi  30522  snelsingles  30760  bj-ax6elem2  31329  bj-spimedv  31386  bj-spimvv  31388  bj-speiv  31391  bj-axrep2  31470  bj-nalset  31475  bj-el  31477  bj-dtru  31478  bj-dvdemo1  31483  bj-dvdemo2  31484  ax6er  31501  bj-vtoclf  31583  wl-exeq  31937  eximp-surprise2  41030
  Copyright terms: Public domain W3C validator