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  2449  exdistrf  2451  sb6x  2468  axc16gALT  2494  raleqOLD  3310  rexeqOLD  3311  vtoclegft  3543  ralxpxfr2d  3600  rr19.3v  3621  rr19.28v  3622  rabtru  3644  moeq3  3670  euxfr2w  3678  euxfr2  3680  reuxfrd  3706  vn0  4297  eq0  4302  ab0orv  4335  dfif3  4494  sseliALT  5254  copsexgw  5438  copsexg  5439  soeq1  5553  frd  5581  soinxp  5706  idrefALT  6070  ordtri3or  6349  nfriotadw  7323  oprabidw  7389  ov6g  7522  ovg  7523  sorpssi  7674  dfxp3  8005  fsplit  8059  frxp3  8093  xpord3inddlem  8096  aceq1  10027  aceq2  10029  axpowndlem4  10511  axpownd  10512  ltsopr  10943  creur  12139  creui  12140  o1fsum  15736  sumodd  16315  sadfval  16379  sadcp1  16382  pceu  16774  vdwlem12  16920  sgrp2rid2ex  18852  gsumval3eu  19833  lss1d  20914  nrmr0reg  23693  stdbdxmet  24459  xrsxmet  24754  cmetcaulem  25244  bcth3  25287  iundisj2  25506  ulmdvlem3  26367  ulmdv  26368  dchrvmasumlem2  27465  colrot1  28631  lnrot1  28695  lnrot2  28696  wlkson  29728  trlsfval  29767  pthsfval  29792  spthsfval  29793  clwlks  29845  crcts  29861  cycls  29862  3cyclfrgrrn1  30360  frgrwopreg  30398  reuxfrdf  32565  iundisj2f  32665  iundisj2fi  32877  constrcbvlem  33912  ordtprsuni  34076  pmeasmono  34481  erdszelem9  35393  satfv1fvfmla1  35617  opnrebl2  36515  wl-ifpimpr  37671  wl-df-3xor  37673  ax12fromc15  39165  axc16g-o  39194  ax12indalem  39205  ax12inda2ALT  39206  dihopelvalcpre  41508  lpolconN  41747  dvrelog2b  42320  isprimroot  42347  aks6d1c2p2  42373  hashscontpow  42376  rspcsbnea  42385  aks6d1c6lem3  42426  fsuppind  42833  zindbi  43188  cnvtrucl0  43865  ismnushort  44542  e2ebind  44804  uunT1  45020  ovnval2  46789  ovnval2b  46796  hoiqssbl  46869  6gbe  48017  8gbe  48019  isgrim  48128  usgrexmpl1tri  48271  gpgov  48288  gpg3kgrtriex  48335