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

Theorem biidd 245
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 244 . 2  |-  ( ps  <->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3anbi12d  1349  3anbi13d  1350  3anbi23d  1351  3anbi1d  1352  3anbi2d  1353  3anbi3d  1354  nfald2  2176  exdistrf  2178  axc16gALT  2207  sb6x  2224  ralxpxfr2d  3176  rr19.3v  3192  rr19.28v  3193  moeq3  3227  euxfr2  3235  dfif3  3907  sseliALT  4550  reuxfr2d  4637  copsexg  4701  soeq1  4793  soinxp  4918  ordtri3or  5474  ov6g  6461  ovg  6462  sorpssi  6604  dfxp3  6880  aceq1  8574  aceq2  8576  axpowndlem4  9051  axpownd  9052  ltsopr  9483  creur  10631  creui  10632  o1fsum  13922  sadfval  14475  sadcp1  14478  pceu  14845  vdwlem12  14991  sgrp2rid2ex  16710  gsumval3eu  17587  lss1d  18235  nrmr0reg  20813  stdbdxmet  21579  xrsxmet  21876  cmetcaulem  22307  bcth3  22348  iundisj2  22551  ulmdvlem3  23406  ulmdv  23407  dchrvmasumlem2  24385  colrot1  24653  lnrot1  24717  lnrot2  24718  dfcgra2  24920  isinag  24928  2pthoncl  25382  crcts  25399  cycls  25400  3cyclfrgrarn1  25789  frgraregorufr0  25829  reuxfr3d  28174  rabtru  28184  iundisj2f  28249  iundisj2fi  28422  ordtprsuni  28774  isrnsigaOLD  28983  pmeasmono  29206  erdszelem9  29971  opnrebl2  31026  wl-ax12  31958  wl-ax11-lem9  31968  ax12  32520  axc16g-o  32550  ax12indalem  32561  ax12inda2ALT  32562  dihopelvalcpre  34861  lpolconN  35100  zindbi  35839  cnvtrucl0  36276  e2ebind  36974  uunT1  37207  trsbcVD  37314  ovnval2  38405  ovnval2b  38412  hoiqssbl  38485  6gbe  38910  8gbe  38912  isrusgr  39629  1wlksfval  39674  1wlk1walk  39697  wlkson  39707  trlsfval  39734  pthsfval  39755  spthsfval  39756  clwlkS  39798  crctS  39811  cyclS  39812
  Copyright terms: Public domain W3C validator