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  1290  3anbi13d  1291  3anbi23d  1292  3anbi1d  1293  3anbi2d  1294  3anbi3d  1295  had1  1444  nfald2  2023  exdistrf  2025  axc16gALT  2056  sb6x  2075  ax12  2205  ax16g-o  2235  ax12indalem  2246  ax12inda2ALT  2247  ralxpxfr2d  3089  rr19.3v  3106  rr19.28v  3107  moeq3  3141  euxfr2  3149  dfif3  3808  sseliALT  4428  reuxfr2d  4520  copsexg  4581  copsexgOLD  4582  soeq1  4665  ordtri3or  4756  soinxp  4908  riotabidv  6059  ov6g  6233  ovg  6234  sorpssi  6371  dfxp3  6639  aceq1  8292  aceq2  8294  axpowndlem4  8771  axpownd  8772  ltsopr  9206  creur  10321  creui  10322  o1fsum  13281  sadfval  13653  sadcp1  13656  pceu  13918  vdwlem12  14058  coafval  14937  gsumval3eu  16386  dprdval  16490  dprdvalOLD  16492  issrg  16614  lss1d  17049  nrmr0reg  19327  stdbdxmet  20095  xrsxmet  20391  cmetcaulem  20804  bcth3  20847  iundisj2  21035  ulmdvlem3  21872  ulmdv  21873  dchrvmasumlem2  22752  istrkgcb  22924  colrot1  22998  lnrot1  23035  lnrot2  23036  israg  23096  eengv  23230  eengtrkg  23236  isausgra  23283  usgraeq12d  23289  usgra0v  23295  usgra1v  23313  2pthoncl  23507  crcts  23513  cycls  23514  reuxfr3d  25878  iundisj2f  25937  fcnvgreu  25996  fpwrelmapffslem  26037  iundisj2fi  26086  isomnd  26169  slmdlema  26224  orngmul  26276  ordtprsuni  26354  nexple  26453  isrnsigaOLD  26560  erdszelem9  27092  wl-ax11-lem9  28414  opnrebl2  28521  zindbi  29292  wwlkn0s  30344  3cyclfrgrarn1  30609  frgraregorufr0  30650  pmattomply1f1  30927  e2ebind  31277  uunT1  31518  trsbcVD  31618  pclfvalN  33538  dihopelvalcpre  34898  lpolconN  35137
  Copyright terms: Public domain W3C validator