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  1436  3anbi13d  1437  3anbi23d  1438  3anbi1d  1439  3anbi2d  1440  3anbi3d  1441  nfald2  2447  exdistrf  2449  sb6x  2466  axc16gALT  2492  raleqOLD  3337  rexeqOLD  3338  vtoclegft  3587  ralxpxfr2d  3645  rr19.3v  3666  rr19.28v  3667  rabtru  3691  moeq3  3720  euxfr2w  3728  euxfr2  3730  reuxfrd  3756  dfif3  4544  sseliALT  5314  copsexgw  5500  copsexg  5501  soeq1  5617  frd  5644  soinxp  5769  idrefALT  6133  ordtri3or  6417  nfriotadw  7395  oprabidw  7461  ov6g  7596  ovg  7597  sorpssi  7747  dfxp3  8084  fsplit  8140  frxp3  8174  xpord3inddlem  8177  aceq1  10154  aceq2  10156  axpowndlem4  10637  axpownd  10638  ltsopr  11069  creur  12257  creui  12258  o1fsum  15845  sumodd  16421  sadfval  16485  sadcp1  16488  pceu  16879  vdwlem12  17025  sgrp2rid2ex  18952  gsumval3eu  19936  lss1d  20978  nrmr0reg  23772  stdbdxmet  24543  xrsxmet  24844  cmetcaulem  25335  bcth3  25378  iundisj2  25597  ulmdvlem3  26459  ulmdv  26460  dchrvmasumlem2  27556  colrot1  28581  lnrot1  28645  lnrot2  28646  wlkson  29688  trlsfval  29727  pthsfval  29753  spthsfval  29754  clwlks  29804  crcts  29820  cycls  29821  3cyclfrgrrn1  30313  frgrwopreg  30351  reuxfrdf  32518  iundisj2f  32609  iundisj2fi  32804  ordtprsuni  33879  pmeasmono  34305  erdszelem9  35183  satfv1fvfmla1  35407  opnrebl2  36303  wl-ifpimpr  37448  wl-df-3xor  37450  wl-ax11-lem9  37573  ax12fromc15  38886  axc16g-o  38915  ax12indalem  38926  ax12inda2ALT  38927  dihopelvalcpre  41230  lpolconN  41469  dvrelog2b  42047  isprimroot  42074  aks6d1c2p2  42100  hashscontpow  42103  rspcsbnea  42112  aks6d1c6lem3  42153  fsuppind  42576  zindbi  42934  cnvtrucl0  43613  ismnushort  44296  e2ebind  44560  uunT1  44777  ovnval2  46500  ovnval2b  46507  hoiqssbl  46580  6gbe  47695  8gbe  47697  isgrim  47805  usgrexmpl1tri  47919  gpgov  47936