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

Theorem biidd 229
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 228 . 2  |-  ( ps  <->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3anbi12d  1255  3anbi13d  1256  3anbi23d  1257  3anbi1d  1258  3anbi2d  1259  3anbi3d  1260  had1  1411  spnfwOLD  1704  spvwOLD  1708  nfald2  2064  exdistrf  2066  exdistrfOLD  2067  sb6x  2121  a16gALT  2156  ax11  2232  a16g-o  2263  ax11indalem  2274  ax11inda2ALT  2275  rr19.3v  3077  rr19.28v  3078  moeq3  3111  euxfr2  3119  dfif3  3749  copsexg  4442  soeq1  4522  ordtri3or  4613  reuxfr2d  4746  soinxp  4942  ov6g  6211  ovg  6212  dfxp3  6406  sorpssi  6528  aceq1  7998  aceq2  8000  axpowndlem4  8475  axpownd  8476  ltsopr  8909  creur  9994  creui  9995  o1fsum  12592  sadfval  12964  sadcp1  12967  pceu  13220  vdwlem12  13360  coafval  14219  gsumval3eu  15513  dprdval  15561  lss1d  16039  nrmr0reg  17781  stdbdxmet  18545  xrsxmet  18840  cmetcaulem  19241  bcth3  19284  iundisj2  19443  ulmdvlem3  20318  ulmdv  20319  dchrvmasumlem2  21192  isausgra  21379  usgraeq12d  21385  usgra0v  21391  usgra1v  21409  2pthoncl  21603  crcts  21609  cycls  21610  reuxfr3d  23976  iundisj2f  24030  iundisj2fi  24153  isrnsigaOLD  24495  erdszelem9  24885  opnrebl2  26324  ralxpxfr2d  26741  zindbi  27009  3cyclfrgrarn1  28402  frgraregorufr0  28441  trsbc  28625  e2ebind  28650  uunT1  28892  trsbcVD  28989  exdistrfNEW7  29505  sb6xNEW7  29629  nfald2OLD7  29717  a16gALTOLD7  29744  pclfvalN  30686  dihopelvalcpre  32046  lpolconN  32285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator