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  3304  rexeqOLD  3305  vtoclegft  3545  ralxpxfr2d  3603  rr19.3v  3624  rr19.28v  3625  rabtru  3647  moeq3  3674  euxfr2w  3682  euxfr2  3684  reuxfrd  3710  dfif3  4493  sseliALT  5251  copsexgw  5437  copsexg  5438  soeq1  5552  frd  5580  soinxp  5705  idrefALT  6066  ordtri3or  6343  nfriotadw  7318  oprabidw  7384  ov6g  7517  ovg  7518  sorpssi  7669  dfxp3  8003  fsplit  8057  frxp3  8091  xpord3inddlem  8094  aceq1  10030  aceq2  10032  axpowndlem4  10513  axpownd  10514  ltsopr  10945  creur  12140  creui  12141  o1fsum  15738  sumodd  16317  sadfval  16381  sadcp1  16384  pceu  16776  vdwlem12  16922  sgrp2rid2ex  18819  gsumval3eu  19801  lss1d  20884  nrmr0reg  23652  stdbdxmet  24419  xrsxmet  24714  cmetcaulem  25204  bcth3  25247  iundisj2  25466  ulmdvlem3  26327  ulmdv  26328  dchrvmasumlem2  27425  colrot1  28522  lnrot1  28586  lnrot2  28587  wlkson  29618  trlsfval  29657  pthsfval  29682  spthsfval  29683  clwlks  29735  crcts  29751  cycls  29752  3cyclfrgrrn1  30247  frgrwopreg  30285  reuxfrdf  32453  iundisj2f  32552  iundisj2fi  32753  constrcbvlem  33724  ordtprsuni  33888  pmeasmono  34294  erdszelem9  35174  satfv1fvfmla1  35398  opnrebl2  36297  wl-ifpimpr  37442  wl-df-3xor  37444  wl-ax11-lem9  37569  ax12fromc15  38886  axc16g-o  38915  ax12indalem  38926  ax12inda2ALT  38927  dihopelvalcpre  41230  lpolconN  41469  dvrelog2b  42042  isprimroot  42069  aks6d1c2p2  42095  hashscontpow  42098  rspcsbnea  42107  aks6d1c6lem3  42148  fsuppind  42566  zindbi  42922  cnvtrucl0  43600  ismnushort  44277  e2ebind  44540  uunT1  44756  ovnval2  46530  ovnval2b  46537  hoiqssbl  46610  6gbe  47759  8gbe  47761  isgrim  47870  usgrexmpl1tri  48013  gpgov  48030  gpg3kgrtriex  48077