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  1658  spvw  1661  exdistrf  1911  nfald2  1912  sb6x  1969  a16gALT  1989  ax11  2094  a16g-o  2125  ax11indalem  2136  ax11inda2ALT  2137  rr19.3v  2909  rr19.28v  2910  moeq3  2942  euxfr2  2950  dfif3  3575  copsexg  4252  soeq1  4333  ordtri3or  4424  reuxfr2d  4557  soinxp  4754  ov6g  5985  ovg  5986  dfxp3  6179  sorpssi  6283  aceq1  7744  aceq2  7746  axpowndlem4  8222  axpownd  8223  ltsopr  8656  creur  9740  creui  9741  o1fsum  12271  sadfval  12643  sadcp1  12646  pceu  12899  vdwlem12  13039  fucsect  13846  coafval  13896  gsumval3eu  15190  dprdval  15238  lss1d  15720  nrmr0reg  17440  stdbdxmet  18061  xrsxmet  18315  cmetcaulem  18714  bcth3  18753  iundisj2  18906  ulmdvlem3  19779  ulmdv  19780  dchrvmasumlem2  20647  reuxfr3d  23138  iundisj2fi  23364  iundisj2f  23366  isrnsigaOLD  23473  measval  23529  erdszelem9  23730  elfuns  24454  altdftru  24948  prismorcset  25914  bisig0  26062  isconcl1b  26097  sgplpte21  26132  sgplpte22  26138  isibcg  26191  opnrebl2  26236  ralxpxfr2d  26760  zindbi  27031  fmul01  27710  stoweidlem19  27768  stoweidlem31  27780  stoweidlem51  27800  stoweidlem52  27801  stoweidlem60  27809  usgraeq12d  28111  usgra0v  28117  usgra1v  28126  cusgra2v  28158  isfrgra  28171  trsbc  28304  e2ebind  28329  uunT1  28555  trsbcVD  28653  ax12-2  29103  ax12-4  29106  pclfvalN  30078  dihopelvalcpre  31438  lpolconN  31677
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