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  1080  3anbi12d  1440  3anbi13d  1441  3anbi23d  1442  3anbi1d  1443  3anbi2d  1444  3anbi3d  1445  nfald2  2450  exdistrf  2452  sb6x  2469  axc16gALT  2495  raleqOLD  3312  rexeqOLD  3313  vtoclegft  3545  ralxpxfr2d  3602  rr19.3v  3623  rr19.28v  3624  rabtru  3646  moeq3  3672  euxfr2w  3680  euxfr2  3682  reuxfrd  3708  vn0  4299  eq0  4304  ab0orv  4337  dfif3  4496  sseliALT  5256  copsexgw  5446  copsexg  5447  soeq1  5561  frd  5589  soinxp  5714  idrefALT  6078  ordtri3or  6357  nfriotadw  7333  oprabidw  7399  ov6g  7532  ovg  7533  sorpssi  7684  dfxp3  8015  fsplit  8069  frxp3  8103  xpord3inddlem  8106  aceq1  10039  aceq2  10041  axpowndlem4  10523  axpownd  10524  ltsopr  10955  creur  12151  creui  12152  o1fsum  15748  sumodd  16327  sadfval  16391  sadcp1  16394  pceu  16786  vdwlem12  16932  sgrp2rid2ex  18864  gsumval3eu  19845  lss1d  20926  nrmr0reg  23705  stdbdxmet  24471  xrsxmet  24766  cmetcaulem  25256  bcth3  25299  iundisj2  25518  ulmdvlem3  26379  ulmdv  26380  dchrvmasumlem2  27477  colrot1  28643  lnrot1  28707  lnrot2  28708  wlkson  29740  trlsfval  29779  pthsfval  29804  spthsfval  29805  clwlks  29857  crcts  29873  cycls  29874  3cyclfrgrrn1  30372  frgrwopreg  30410  reuxfrdf  32576  iundisj2f  32676  iundisj2fi  32887  constrcbvlem  33932  ordtprsuni  34096  pmeasmono  34501  erdszelem9  35412  satfv1fvfmla1  35636  opnrebl2  36534  wl-ifpimpr  37718  wl-df-3xor  37720  ax12fromc15  39278  axc16g-o  39307  ax12indalem  39318  ax12inda2ALT  39319  dihopelvalcpre  41621  lpolconN  41860  dvrelog2b  42433  isprimroot  42460  aks6d1c2p2  42486  hashscontpow  42489  rspcsbnea  42498  aks6d1c6lem3  42539  fsuppind  42945  zindbi  43300  cnvtrucl0  43977  ismnushort  44654  e2ebind  44916  uunT1  45132  ovnval2  46900  ovnval2b  46907  hoiqssbl  46980  6gbe  48128  8gbe  48130  isgrim  48239  usgrexmpl1tri  48382  gpgov  48399  gpg3kgrtriex  48446