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

Theorem eximii 1709
Description: Inference associated with eximi 1707. (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 1707 . 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 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-ex 1664
This theorem is referenced by:  exiftru  1808  spimeh  1841  equidOLD  1856  ax6evr  1859  spimv1  2058  cbv3hvOLD  2062  cbv3hvOLDOLD  2063  ax6e  2094  spim  2098  spimed  2099  spimv  2101  spei  2105  equvini  2179  equveli  2180  euequ1  2305  euex  2323  darii  2394  barbari  2396  festino  2400  baroco  2401  cesaro  2402  camestros  2403  datisi  2404  disamis  2405  felapton  2408  darapti  2409  dimatis  2411  fresison  2412  calemos  2413  fesapo  2414  bamalip  2415  vtoclf  3099  vtocl  3100  axrep2  4517  axnul  4532  nalset  4540  notzfaus  4578  el  4585  dtru  4594  eusv2nf  4601  dvdemo1  4635  dvdemo2  4636  axpr  4638  snnex  6597  inf1  8127  bnd  8363  axpowndlem2  9023  grothomex  9254  bnj101  29529  axextdfeq  30444  ax8dfeq  30445  axextndbi  30451  snelsingles  30689  bj-ax6elem2  31265  bj-spimedv  31320  bj-spimvv  31322  bj-speiv  31325  bj-axrep2  31404  bj-nalset  31409  bj-el  31411  bj-dtru  31412  bj-dvdemo1  31417  bj-dvdemo2  31418  ax6er  31435  bj-vtoclf  31515  wl-exeq  31867  eximp-surprise2  40577
  Copyright terms: Public domain W3C validator