Theorem biidd 261

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 260	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ifpbi23d  1077  3anbi12d  1433  3anbi13d  1434  3anbi23d  1435  3anbi1d  1436  3anbi2d  1437  3anbi3d  1438  nfald2  2438  exdistrf  2440  sb6x  2457  axc16gALT  2483  raleqOLD  3324  rexeqOLD  3325  vtoclegft  3568  ralxpxfr2d  3629  rr19.3v  3652  rr19.28v  3653  rabtru  3676  moeq3  3704  euxfr2w  3712  euxfr2  3714  reuxfrd  3740  dfif3  4544  sseliALT  5310  copsexgw  5492  copsexg  5493  soeq1  5611  frd  5637  soinxp  5759  idrefALT  6118  ordtri3or  6403  nfriotadw  7383  oprabidw  7450  ov6g  7585  ovg  7586  sorpssi  7735  dfxp3  8066  fsplit  8122  frxp3  8156  xpord3inddlem  8159  aceq1  10142  aceq2  10144  axpowndlem4  10625  axpownd  10626  ltsopr  11057  creur  12239  creui  12240  o1fsum  15795  sumodd  16368  sadfval  16430  sadcp1  16433  pceu  16818  vdwlem12  16964  sgrp2rid2ex  18887  gsumval3eu  19871  lss1d  20859  nrmr0reg  23697  stdbdxmet  24468  xrsxmet  24769  cmetcaulem  25260  bcth3  25303  iundisj2  25522  ulmdvlem3  26383  ulmdv  26384  dchrvmasumlem2  27476  colrot1  28435  lnrot1  28499  lnrot2  28500  wlkson  29542  trlsfval  29581  pthsfval  29607  spthsfval  29608  clwlks  29658  crcts  29674  cycls  29675  3cyclfrgrrn1  30167  frgrwopreg  30205  reuxfrdf  32367  iundisj2f  32459  iundisj2fi  32647  ordtprsuni  33648  pmeasmono  34072  erdszelem9  34937  satfv1fvfmla1  35161  opnrebl2  35933  wl-ifpimpr  37073  wl-df-3xor  37075  wl-ax11-lem9  37188  ax12fromc15  38504  axc16g-o  38533  ax12indalem  38544  ax12inda2ALT  38545  dihopelvalcpre  40848  lpolconN  41087  dvrelog2b  41666  isprimroot  41693  aks6d1c2p2  41719  hashscontpow  41722  rspcsbnea  41731  sticksstones11  41756  aks6d1c6lem3  41772  fsuppind  41955  zindbi  42506  cnvtrucl0  43193  ismnushort  43877  e2ebind  44141  uunT1  44358  ovnval2  46068  ovnval2b  46075  hoiqssbl  46148  6gbe  47245  8gbe  47247  isgrim  47349