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  1080  3anbi12d  1440  3anbi13d  1441  3anbi23d  1442  3anbi1d  1443  3anbi2d  1444  3anbi3d  1445  nfald2  2450  exdistrf  2452  sb6x  2469  axc16gALT  2495  vtoclegft  3532  ralxpxfr2d  3589  rr19.3v  3610  rr19.28v  3611  rabtru  3633  moeq3  3659  euxfr2w  3667  euxfr2  3669  reuxfrd  3695  vn0  4286  eq0  4291  ab0orv  4324  dfif3  4482  sseliALT  5244  copsexgw  5438  copsexg  5439  soeq1  5553  frd  5581  soinxp  5706  idrefALT  6070  ordtri3or  6349  nfriotadw  7325  oprabidw  7391  ov6g  7524  ovg  7525  sorpssi  7676  dfxp3  8007  fsplit  8060  frxp3  8094  xpord3inddlem  8097  aceq1  10030  aceq2  10032  axpowndlem4  10514  axpownd  10515  ltsopr  10946  creur  12144  creui  12145  o1fsum  15767  sumodd  16348  sadfval  16412  sadcp1  16415  pceu  16808  vdwlem12  16954  sgrp2rid2ex  18889  gsumval3eu  19870  lss1d  20949  nrmr0reg  23724  stdbdxmet  24490  xrsxmet  24785  cmetcaulem  25265  bcth3  25308  iundisj2  25526  ulmdvlem3  26380  ulmdv  26381  dchrvmasumlem2  27475  colrot1  28641  lnrot1  28705  lnrot2  28706  wlkson  29738  trlsfval  29777  pthsfval  29802  spthsfval  29803  clwlks  29855  crcts  29871  cycls  29872  3cyclfrgrrn1  30370  frgrwopreg  30408  reuxfrdf  32575  iundisj2f  32675  iundisj2fi  32885  constrcbvlem  33915  ordtprsuni  34079  pmeasmono  34484  erdszelem9  35397  satfv1fvfmla1  35621  opnrebl2  36519  wl-ifpimpr  37796  wl-df-3xor  37798  ax12fromc15  39365  axc16g-o  39394  ax12indalem  39405  ax12inda2ALT  39406  dihopelvalcpre  41708  lpolconN  41947  dvrelog2b  42519  isprimroot  42546  aks6d1c2p2  42572  hashscontpow  42575  rspcsbnea  42584  aks6d1c6lem3  42625  fsuppind  43037  zindbi  43392  cnvtrucl0  44069  ismnushort  44746  e2ebind  45008  uunT1  45224  ovnval2  46991  ovnval2b  46998  hoiqssbl  47071  6gbe  48259  8gbe  48261  isgrim  48370  usgrexmpl1tri  48513  gpgov  48530  gpg3kgrtriex  48577