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  1080  3anbi12d  1437  3anbi13d  1438  3anbi23d  1439  3anbi1d  1440  3anbi2d  1441  3anbi3d  1442  nfald2  2444  exdistrf  2446  sb6x  2463  axc16gALT  2489  raleqOLD  3335  rexeqOLD  3336  vtoclegft  3573  ralxpxfr2d  3633  rr19.3v  3656  rr19.28v  3657  rabtru  3679  moeq3  3707  euxfr2w  3715  euxfr2  3717  reuxfrd  3743  dfif3  4541  sseliALT  5308  copsexgw  5489  copsexg  5490  soeq1  5608  frd  5634  soinxp  5755  idrefALT  6109  ordtri3or  6393  nfriotadw  7369  oprabidw  7436  ov6g  7567  ovg  7568  sorpssi  7715  dfxp3  8043  fsplit  8099  frxp3  8133  xpord3inddlem  8136  aceq1  10108  aceq2  10110  axpowndlem4  10591  axpownd  10592  ltsopr  11023  creur  12202  creui  12203  o1fsum  15755  sumodd  16327  sadfval  16389  sadcp1  16392  pceu  16775  vdwlem12  16921  sgrp2rid2ex  18804  gsumval3eu  19766  lss1d  20566  nrmr0reg  23244  stdbdxmet  24015  xrsxmet  24316  cmetcaulem  24796  bcth3  24839  iundisj2  25057  ulmdvlem3  25905  ulmdv  25906  dchrvmasumlem2  26990  colrot1  27799  lnrot1  27863  lnrot2  27864  wlkson  28902  trlsfval  28941  pthsfval  28967  spthsfval  28968  clwlks  29018  crcts  29034  cycls  29035  3cyclfrgrrn1  29527  frgrwopreg  29565  reuxfrdf  31718  iundisj2f  31808  iundisj2fi  31995  ordtprsuni  32887  pmeasmono  33311  erdszelem9  34178  satfv1fvfmla1  34402  opnrebl2  35194  wl-ifpimpr  36335  wl-df-3xor  36337  wl-ax11-lem9  36443  ax12fromc15  37763  axc16g-o  37792  ax12indalem  37803  ax12inda2ALT  37804  dihopelvalcpre  40107  lpolconN  40346  dvrelog2b  40919  aks6d1c2p2  40945  sticksstones11  40960  fsuppind  41159  zindbi  41670  cnvtrucl0  42360  ismnushort  43045  e2ebind  43309  uunT1  43526  ovnval2  45247  ovnval2b  45254  hoiqssbl  45327  6gbe  46425  8gbe  46427