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  1298  3anbi13d  1299  3anbi23d  1300  3anbi1d  1301  3anbi2d  1302  3anbi3d  1303  had1  1478  nfald2  2079  exdistrf  2081  axc16gALT  2110  sb6x  2129  ralxpxfr2d  3149  rr19.3v  3166  rr19.28v  3167  moeq3  3201  euxfr2  3209  dfif3  3871  sseliALT  4498  reuxfr2d  4585  copsexg  4647  soeq1  4733  ordtri3or  4824  soinxp  4978  ov6g  6339  ovg  6340  sorpssi  6485  dfxp3  6759  aceq1  8411  aceq2  8413  axpowndlem4  8888  axpownd  8889  ltsopr  9321  creur  10446  creui  10447  o1fsum  13629  sadfval  14104  sadcp1  14107  pceu  14372  vdwlem12  14512  coafval  15460  sgrp2rid2ex  16162  gsumval3eu  17024  dprdval  17147  dprdvalOLD  17149  lss1d  17722  nrmr0reg  20335  stdbdxmet  21103  xrsxmet  21399  cmetcaulem  21812  bcth3  21855  iundisj2  22044  ulmdvlem3  22882  ulmdv  22883  dchrvmasumlem2  23800  colrot1  24066  lnrot1  24123  lnrot2  24124  eengv  24403  isausgra  24475  usgraeq12d  24483  usgra0v  24492  usgra1v  24511  2pthoncl  24726  crcts  24743  cycls  24744  3cyclfrgrarn1  25133  frgraregorufr0  25173  reuxfr3d  27505  rabtru  27517  iundisj2f  27579  iundisj2fi  27755  ordtprsuni  28055  isrnsigaOLD  28261  erdszelem9  28832  mpstval  29084  wl-ax11-lem9  30198  opnrebl2  30305  zindbi  31047  e2ebind  33676  uunT1  33917  trsbcVD  34024  ax12  35047  ax16g-o  35077  ax12indalem  35088  ax12inda2ALT  35089  pclfvalN  36026  dihopelvalcpre  37388  lpolconN  37627
  Copyright terms: Public domain W3C validator