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  2444  exdistrf  2446  sb6x  2463  axc16gALT  2489  raleqOLD  3315  rexeqOLD  3316  vtoclegft  3557  ralxpxfr2d  3615  rr19.3v  3636  rr19.28v  3637  rabtru  3659  moeq3  3686  euxfr2w  3694  euxfr2  3696  reuxfrd  3722  dfif3  4506  sseliALT  5267  copsexgw  5453  copsexg  5454  soeq1  5570  frd  5598  soinxp  5723  idrefALT  6087  ordtri3or  6367  nfriotadw  7355  oprabidw  7421  ov6g  7556  ovg  7557  sorpssi  7708  dfxp3  8043  fsplit  8099  frxp3  8133  xpord3inddlem  8136  aceq1  10077  aceq2  10079  axpowndlem4  10560  axpownd  10561  ltsopr  10992  creur  12187  creui  12188  o1fsum  15786  sumodd  16365  sadfval  16429  sadcp1  16432  pceu  16824  vdwlem12  16970  sgrp2rid2ex  18861  gsumval3eu  19841  lss1d  20876  nrmr0reg  23643  stdbdxmet  24410  xrsxmet  24705  cmetcaulem  25195  bcth3  25238  iundisj2  25457  ulmdvlem3  26318  ulmdv  26319  dchrvmasumlem2  27416  colrot1  28493  lnrot1  28557  lnrot2  28558  wlkson  29591  trlsfval  29630  pthsfval  29656  spthsfval  29657  clwlks  29709  crcts  29725  cycls  29726  3cyclfrgrrn1  30221  frgrwopreg  30259  reuxfrdf  32427  iundisj2f  32526  iundisj2fi  32727  constrcbvlem  33752  ordtprsuni  33916  pmeasmono  34322  erdszelem9  35193  satfv1fvfmla1  35417  opnrebl2  36316  wl-ifpimpr  37461  wl-df-3xor  37463  wl-ax11-lem9  37588  ax12fromc15  38905  axc16g-o  38934  ax12indalem  38945  ax12inda2ALT  38946  dihopelvalcpre  41249  lpolconN  41488  dvrelog2b  42061  isprimroot  42088  aks6d1c2p2  42114  hashscontpow  42117  rspcsbnea  42126  aks6d1c6lem3  42167  fsuppind  42585  zindbi  42942  cnvtrucl0  43620  ismnushort  44297  e2ebind  44560  uunT1  44776  ovnval2  46550  ovnval2b  46557  hoiqssbl  46630  6gbe  47776  8gbe  47778  isgrim  47886  usgrexmpl1tri  48020  gpgov  48037  gpg3kgrtriex  48084