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 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  1081  3anbi12d  1438  3anbi13d  1439  3anbi23d  1440  3anbi1d  1441  3anbi2d  1442  3anbi3d  1443  nfald2  2445  exdistrf  2447  sb6x  2464  axc16gALT  2490  raleqOLD  3336  rexeqOLD  3337  vtoclegft  3574  ralxpxfr2d  3635  rr19.3v  3658  rr19.28v  3659  rabtru  3681  moeq3  3709  euxfr2w  3717  euxfr2  3719  reuxfrd  3745  dfif3  4543  sseliALT  5310  copsexgw  5491  copsexg  5492  soeq1  5610  frd  5636  soinxp  5758  idrefALT  6113  ordtri3or  6397  nfriotadw  7373  oprabidw  7440  ov6g  7571  ovg  7572  sorpssi  7719  dfxp3  8047  fsplit  8103  frxp3  8137  xpord3inddlem  8140  aceq1  10112  aceq2  10114  axpowndlem4  10595  axpownd  10596  ltsopr  11027  creur  12206  creui  12207  o1fsum  15759  sumodd  16331  sadfval  16393  sadcp1  16396  pceu  16779  vdwlem12  16925  sgrp2rid2ex  18808  gsumval3eu  19772  lss1d  20574  nrmr0reg  23253  stdbdxmet  24024  xrsxmet  24325  cmetcaulem  24805  bcth3  24848  iundisj2  25066  ulmdvlem3  25914  ulmdv  25915  dchrvmasumlem2  27001  colrot1  27810  lnrot1  27874  lnrot2  27875  wlkson  28913  trlsfval  28952  pthsfval  28978  spthsfval  28979  clwlks  29029  crcts  29045  cycls  29046  3cyclfrgrrn1  29538  frgrwopreg  29576  reuxfrdf  31731  iundisj2f  31821  iundisj2fi  32008  ordtprsuni  32899  pmeasmono  33323  erdszelem9  34190  satfv1fvfmla1  34414  opnrebl2  35206  wl-ifpimpr  36347  wl-df-3xor  36349  wl-ax11-lem9  36455  ax12fromc15  37775  axc16g-o  37804  ax12indalem  37815  ax12inda2ALT  37816  dihopelvalcpre  40119  lpolconN  40358  dvrelog2b  40931  aks6d1c2p2  40957  sticksstones11  40972  fsuppind  41162  zindbi  41685  cnvtrucl0  42375  ismnushort  43060  e2ebind  43324  uunT1  43541  ovnval2  45261  ovnval2b  45268  hoiqssbl  45341  6gbe  46439  8gbe  46441