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

Theorem biidd 237
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
Assertion
Ref Expression
biidd  |-  ( ph  ->  ( ps  <->  ps )
)

Proof of Theorem biidd
StepHypRef Expression
1 biid 236 . 2  |-  ( ps  <->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  3anbi12d  1300  3anbi13d  1301  3anbi23d  1302  3anbi1d  1303  3anbi2d  1304  3anbi3d  1305  had1  1454  nfald2  2046  exdistrf  2048  axc16gALT  2079  sb6x  2098  ax12  2227  ax16g-o  2257  ax12indalem  2268  ax12inda2ALT  2269  ralxpxfr2d  3228  rr19.3v  3245  rr19.28v  3246  moeq3  3280  euxfr2  3288  dfif3  3953  sseliALT  4578  reuxfr2d  4670  copsexg  4732  copsexgOLD  4733  soeq1  4819  ordtri3or  4910  soinxp  5064  riotabidv  6247  ov6g  6424  ovg  6425  sorpssi  6570  dfxp3  6844  aceq1  8498  aceq2  8500  axpowndlem4  8977  axpownd  8978  ltsopr  9410  creur  10530  creui  10531  o1fsum  13590  sadfval  13961  sadcp1  13964  pceu  14229  vdwlem12  14369  coafval  15249  gsumval3eu  16710  dprdval  16837  dprdvalOLD  16839  issrg  16961  lss1d  17409  nrmr0reg  20013  stdbdxmet  20781  xrsxmet  21077  cmetcaulem  21490  bcth3  21533  iundisj2  21722  ulmdvlem3  22559  ulmdv  22560  dchrvmasumlem2  23439  istrkgcb  23609  colrot1  23702  lnrot1  23745  lnrot2  23746  israg  23810  eengv  23986  eengtrkg  23992  isausgra  24058  usgraeq12d  24066  usgra0v  24075  usgra1v  24094  2pthoncl  24309  crcts  24326  cycls  24327  wwlkn0s  24409  3cyclfrgrarn1  24716  frgraregorufr0  24757  reuxfr3d  27092  iundisj2f  27150  fcnvgreu  27214  fpwrelmapffslem  27255  iundisj2fi  27298  isomnd  27381  slmdlema  27436  orngmul  27484  ordtprsuni  27565  nexple  27673  isrnsigaOLD  27780  erdszelem9  28311  wl-ax11-lem9  29638  opnrebl2  29744  zindbi  30514  sgrpplusgaop  31962  e2ebind  32434  uunT1  32675  trsbcVD  32775  pclfvalN  34703  dihopelvalcpre  36063  lpolconN  36302
  Copyright terms: Public domain W3C validator