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  2443  exdistrf  2445  sb6x  2462  axc16gALT  2488  raleqOLD  3313  rexeqOLD  3314  vtoclegft  3554  ralxpxfr2d  3612  rr19.3v  3633  rr19.28v  3634  rabtru  3656  moeq3  3683  euxfr2w  3691  euxfr2  3693  reuxfrd  3719  dfif3  4503  sseliALT  5264  copsexgw  5450  copsexg  5451  soeq1  5567  frd  5595  soinxp  5720  idrefALT  6084  ordtri3or  6364  nfriotadw  7352  oprabidw  7418  ov6g  7553  ovg  7554  sorpssi  7705  dfxp3  8040  fsplit  8096  frxp3  8130  xpord3inddlem  8133  aceq1  10070  aceq2  10072  axpowndlem4  10553  axpownd  10554  ltsopr  10985  creur  12180  creui  12181  o1fsum  15779  sumodd  16358  sadfval  16422  sadcp1  16425  pceu  16817  vdwlem12  16963  sgrp2rid2ex  18854  gsumval3eu  19834  lss1d  20869  nrmr0reg  23636  stdbdxmet  24403  xrsxmet  24698  cmetcaulem  25188  bcth3  25231  iundisj2  25450  ulmdvlem3  26311  ulmdv  26312  dchrvmasumlem2  27409  colrot1  28486  lnrot1  28550  lnrot2  28551  wlkson  29584  trlsfval  29623  pthsfval  29649  spthsfval  29650  clwlks  29702  crcts  29718  cycls  29719  3cyclfrgrrn1  30214  frgrwopreg  30252  reuxfrdf  32420  iundisj2f  32519  iundisj2fi  32720  constrcbvlem  33745  ordtprsuni  33909  pmeasmono  34315  erdszelem9  35186  satfv1fvfmla1  35410  opnrebl2  36309  wl-ifpimpr  37454  wl-df-3xor  37456  wl-ax11-lem9  37581  ax12fromc15  38898  axc16g-o  38927  ax12indalem  38938  ax12inda2ALT  38939  dihopelvalcpre  41242  lpolconN  41481  dvrelog2b  42054  isprimroot  42081  aks6d1c2p2  42107  hashscontpow  42110  rspcsbnea  42119  aks6d1c6lem3  42160  fsuppind  42578  zindbi  42935  cnvtrucl0  43613  ismnushort  44290  e2ebind  44553  uunT1  44769  ovnval2  46543  ovnval2b  46550  hoiqssbl  46623  6gbe  47772  8gbe  47774  isgrim  47882  usgrexmpl1tri  48016  gpgov  48033  gpg3kgrtriex  48080