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

Theorem biidd 228
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 227 . 2  |-  ( ps  <->  ps )
21a1i 10 1  |-  ( ph  ->  ( ps  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3anbi12d  1253  3anbi13d  1254  3anbi23d  1255  3anbi1d  1256  3anbi2d  1257  3anbi3d  1258  had1  1392  spnfwOLD  1677  spvwOLD  1680  exdistrf  1924  nfald2  1925  sb6x  1982  a16gALT  2002  ax11  2107  a16g-o  2138  ax11indalem  2149  ax11inda2ALT  2150  rr19.3v  2922  rr19.28v  2923  moeq3  2955  euxfr2  2963  dfif3  3588  copsexg  4268  soeq1  4349  ordtri3or  4440  reuxfr2d  4573  soinxp  4770  ov6g  6001  ovg  6002  dfxp3  6195  sorpssi  6299  aceq1  7760  aceq2  7762  axpowndlem4  8238  axpownd  8239  ltsopr  8672  creur  9756  creui  9757  o1fsum  12287  sadfval  12659  sadcp1  12662  pceu  12915  vdwlem12  13055  fucsect  13862  coafval  13912  gsumval3eu  15206  dprdval  15254  lss1d  15736  nrmr0reg  17456  stdbdxmet  18077  xrsxmet  18331  cmetcaulem  18730  bcth3  18769  iundisj2  18922  ulmdvlem3  19795  ulmdv  19796  dchrvmasumlem2  20663  reuxfr3d  23154  iundisj2fi  23379  iundisj2f  23381  isrnsigaOLD  23488  measval  23544  erdszelem9  23745  elfuns  24525  altdftru  25051  prismorcset  26017  bisig0  26165  isconcl1b  26200  sgplpte21  26235  sgplpte22  26241  isibcg  26294  opnrebl2  26339  ralxpxfr2d  26863  zindbi  27134  fmul01  27813  stoweidlem19  27871  stoweidlem31  27883  stoweidlem51  27903  stoweidlem52  27904  stoweidlem60  27912  usgraeq12d  28245  usgra0v  28251  usgra1v  28260  nb3graprlem2  28288  cusgra2v  28297  crcts  28367  cycls  28368  isfrgra  28417  3cyclfrgrarn1  28435  trsbc  28603  e2ebind  28628  uunT1  28869  trsbcVD  28969  exdistrfNEW7  29482  sb6xNEW7  29601  nfald2OLD7  29671  a16gALTOLD7  29698  ax12-2  29725  ax12-4  29728  pclfvalN  30700  dihopelvalcpre  32060  lpolconN  32299
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 177
  Copyright terms: Public domain W3C validator