Theorem biidd 262

Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)

Assertion

Ref	Expression
biidd	⊢ (𝜑 → (𝜓 ↔ 𝜓))

Proof of Theorem biidd

Step	Hyp	Ref	Expression
1		biid 261	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ifpbi23d  1079  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  3anbi1d  1442  3anbi2d  1443  3anbi3d  1444  nfald2  2449  exdistrf  2451  sb6x  2468  axc16gALT  2494  raleqOLD  3319  rexeqOLD  3320  vtoclegft  3567  ralxpxfr2d  3625  rr19.3v  3646  rr19.28v  3647  rabtru  3668  moeq3  3695  euxfr2w  3703  euxfr2  3705  reuxfrd  3731  dfif3  4515  sseliALT  5279  copsexgw  5465  copsexg  5466  soeq1  5582  frd  5610  soinxp  5736  idrefALT  6100  ordtri3or  6384  nfriotadw  7370  oprabidw  7436  ov6g  7571  ovg  7572  sorpssi  7723  dfxp3  8060  fsplit  8116  frxp3  8150  xpord3inddlem  8153  aceq1  10131  aceq2  10133  axpowndlem4  10614  axpownd  10615  ltsopr  11046  creur  12234  creui  12235  o1fsum  15829  sumodd  16407  sadfval  16471  sadcp1  16474  pceu  16866  vdwlem12  17012  sgrp2rid2ex  18905  gsumval3eu  19885  lss1d  20920  nrmr0reg  23687  stdbdxmet  24454  xrsxmet  24749  cmetcaulem  25240  bcth3  25283  iundisj2  25502  ulmdvlem3  26363  ulmdv  26364  dchrvmasumlem2  27461  colrot1  28538  lnrot1  28602  lnrot2  28603  wlkson  29636  trlsfval  29675  pthsfval  29701  spthsfval  29702  clwlks  29754  crcts  29770  cycls  29771  3cyclfrgrrn1  30266  frgrwopreg  30304  reuxfrdf  32472  iundisj2f  32571  iundisj2fi  32774  constrcbvlem  33789  ordtprsuni  33950  pmeasmono  34356  erdszelem9  35221  satfv1fvfmla1  35445  opnrebl2  36339  wl-ifpimpr  37484  wl-df-3xor  37486  wl-ax11-lem9  37611  ax12fromc15  38923  axc16g-o  38952  ax12indalem  38963  ax12inda2ALT  38964  dihopelvalcpre  41267  lpolconN  41506  dvrelog2b  42079  isprimroot  42106  aks6d1c2p2  42132  hashscontpow  42135  rspcsbnea  42144  aks6d1c6lem3  42185  fsuppind  42613  zindbi  42970  cnvtrucl0  43648  ismnushort  44325  e2ebind  44588  uunT1  44804  ovnval2  46574  ovnval2b  46581  hoiqssbl  46654  6gbe  47785  8gbe  47787  isgrim  47895  usgrexmpl1tri  48029  gpgov  48046  gpg3kgrtriex  48091