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  2447  exdistrf  2449  sb6x  2466  axc16gALT  2492  raleqOLD  3307  rexeqOLD  3308  vtoclegft  3540  ralxpxfr2d  3597  rr19.3v  3618  rr19.28v  3619  rabtru  3641  moeq3  3667  euxfr2w  3675  euxfr2  3677  reuxfrd  3703  vn0  4294  eq0  4299  ab0orv  4332  dfif3  4491  sseliALT  5251  copsexgw  5435  copsexg  5436  soeq1  5550  frd  5578  soinxp  5703  idrefALT  6066  ordtri3or  6345  nfriotadw  7319  oprabidw  7385  ov6g  7518  ovg  7519  sorpssi  7670  dfxp3  8001  fsplit  8055  frxp3  8089  xpord3inddlem  8092  aceq1  10017  aceq2  10019  axpowndlem4  10500  axpownd  10501  ltsopr  10932  creur  12128  creui  12129  o1fsum  15724  sumodd  16303  sadfval  16367  sadcp1  16370  pceu  16762  vdwlem12  16908  sgrp2rid2ex  18839  gsumval3eu  19820  lss1d  20900  nrmr0reg  23667  stdbdxmet  24433  xrsxmet  24728  cmetcaulem  25218  bcth3  25261  iundisj2  25480  ulmdvlem3  26341  ulmdv  26342  dchrvmasumlem2  27439  colrot1  28540  lnrot1  28604  lnrot2  28605  wlkson  29637  trlsfval  29676  pthsfval  29701  spthsfval  29702  clwlks  29754  crcts  29770  cycls  29771  3cyclfrgrrn1  30269  frgrwopreg  30307  reuxfrdf  32474  iundisj2f  32574  iundisj2fi  32786  constrcbvlem  33791  ordtprsuni  33955  pmeasmono  34360  erdszelem9  35266  satfv1fvfmla1  35490  opnrebl2  36388  wl-ifpimpr  37533  wl-df-3xor  37535  ax12fromc15  39027  axc16g-o  39056  ax12indalem  39067  ax12inda2ALT  39068  dihopelvalcpre  41370  lpolconN  41609  dvrelog2b  42182  isprimroot  42209  aks6d1c2p2  42235  hashscontpow  42238  rspcsbnea  42247  aks6d1c6lem3  42288  fsuppind  42711  zindbi  43066  cnvtrucl0  43744  ismnushort  44421  e2ebind  44683  uunT1  44899  ovnval2  46670  ovnval2b  46677  hoiqssbl  46750  6gbe  47898  8gbe  47900  isgrim  48009  usgrexmpl1tri  48152  gpgov  48169  gpg3kgrtriex  48216