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

Theorem eximii 1637
Description: Inference associated with eximi 1635. (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 1635 . 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 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  exiftru  1722  spimeh  1731  equid  1740  cbv3hv  1903  ax6e  1971  spim  1975  spimed  1976  spei  1981  equvini  2060  equveli  2061  equveliOLD  2062  2ax6elem  2179  euequ1  2281  euex  2303  darii  2408  barbari  2410  festino  2414  baroco  2415  cesaro  2416  camestros  2417  datisi  2418  disamis  2419  felapton  2422  darapti  2423  dimatis  2425  fresison  2426  calemos  2427  fesapo  2428  bamalip  2429  vtoclf  3169  axrep2  4566  nalset  4590  notzfaus  4628  el  4635  dtru  4644  eusv2nf  4651  dvdemo1  4688  dvdemo2  4689  axpr  4691  snnex  6601  inf1  8051  bnd  8322  grothomex  9219  axextdfeq  29157  ax8dfeq  29158  axextndbi  29164  snelsingles  29499  wl-exeq  29914  eximp-surprise2  32682  bnj101  33257  bj-spimv  33762  bj-spimedv  33763  bj-speiv  33768  bj-axrep2  33857  bj-nalset  33862  bj-el  33864  bj-dtru  33865  bj-dvdemo1  33870  bj-dvdemo2  33871  ax6er  33888  bj-vtoclf  33962
  Copyright terms: Public domain W3C validator