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  1078  3anbi12d  1435  3anbi13d  1436  3anbi23d  1437  3anbi1d  1438  3anbi2d  1439  3anbi3d  1440  nfald2  2445  exdistrf  2447  sb6x  2464  axc16gALT  2494  raleq  3333  rexeq  3334  ralxpxfr2d  3568  rr19.3v  3591  rr19.28v  3592  rabtru  3614  moeq3  3642  euxfr2w  3650  euxfr2  3652  reuxfrd  3678  dfif3  4470  sseliALT  5228  copsexgw  5398  copsexg  5399  soeq1  5515  frd  5539  soinxp  5659  idrefALT  6007  ordtri3or  6283  nfriotadw  7220  oprabidw  7286  ov6g  7414  ovg  7415  sorpssi  7560  dfxp3  7874  fsplit  7928  aceq1  9804  aceq2  9806  axpowndlem4  10287  axpownd  10288  ltsopr  10719  creur  11897  creui  11898  o1fsum  15453  sumodd  16025  sadfval  16087  sadcp1  16090  pceu  16475  vdwlem12  16621  sgrp2rid2ex  18481  gsumval3eu  19420  lss1d  20140  nrmr0reg  22808  stdbdxmet  23577  xrsxmet  23878  cmetcaulem  24357  bcth3  24400  iundisj2  24618  ulmdvlem3  25466  ulmdv  25467  dchrvmasumlem2  26551  colrot1  26824  lnrot1  26888  lnrot2  26889  wlkson  27926  trlsfval  27965  pthsfval  27990  spthsfval  27991  clwlks  28041  crcts  28057  cycls  28058  3cyclfrgrrn1  28550  frgrwopreg  28588  reuxfrdf  30740  iundisj2f  30830  iundisj2fi  31020  ordtprsuni  31771  pmeasmono  32191  erdszelem9  33061  satfv1fvfmla1  33285  xpord3ind  33727  opnrebl2  34437  wl-ifpimpr  35564  wl-df-3xor  35566  wl-ax11-lem9  35671  ax12fromc15  36846  axc16g-o  36875  ax12indalem  36886  ax12inda2ALT  36887  dihopelvalcpre  39189  lpolconN  39428  dvrelog2b  40002  sticksstones11  40040  fsuppind  40202  zindbi  40684  cnvtrucl0  41121  ismnushort  41808  e2ebind  42072  uunT1  42289  ovnval2  43973  ovnval2b  43980  hoiqssbl  44053  6gbe  45111  8gbe  45113