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  2445  exdistrf  2447  sb6x  2464  axc16gALT  2490  raleqOLD  3306  rexeqOLD  3307  vtoclegft  3543  ralxpxfr2d  3601  rr19.3v  3622  rr19.28v  3623  rabtru  3645  moeq3  3671  euxfr2w  3679  euxfr2  3681  reuxfrd  3707  dfif3  4490  sseliALT  5247  copsexgw  5430  copsexg  5431  soeq1  5545  frd  5573  soinxp  5698  idrefALT  6060  ordtri3or  6338  nfriotadw  7311  oprabidw  7377  ov6g  7510  ovg  7511  sorpssi  7662  dfxp3  7993  fsplit  8047  frxp3  8081  xpord3inddlem  8084  aceq1  10008  aceq2  10010  axpowndlem4  10491  axpownd  10492  ltsopr  10923  creur  12119  creui  12120  o1fsum  15720  sumodd  16299  sadfval  16363  sadcp1  16366  pceu  16758  vdwlem12  16904  sgrp2rid2ex  18835  gsumval3eu  19817  lss1d  20897  nrmr0reg  23665  stdbdxmet  24431  xrsxmet  24726  cmetcaulem  25216  bcth3  25259  iundisj2  25478  ulmdvlem3  26339  ulmdv  26340  dchrvmasumlem2  27437  colrot1  28538  lnrot1  28602  lnrot2  28603  wlkson  29634  trlsfval  29673  pthsfval  29698  spthsfval  29699  clwlks  29751  crcts  29767  cycls  29768  3cyclfrgrrn1  30263  frgrwopreg  30301  reuxfrdf  32468  iundisj2f  32568  iundisj2fi  32777  constrcbvlem  33766  ordtprsuni  33930  pmeasmono  34335  erdszelem9  35241  satfv1fvfmla1  35465  opnrebl2  36361  wl-ifpimpr  37506  wl-df-3xor  37508  wl-ax11-lem9  37633  ax12fromc15  38950  axc16g-o  38979  ax12indalem  38990  ax12inda2ALT  38991  dihopelvalcpre  41293  lpolconN  41532  dvrelog2b  42105  isprimroot  42132  aks6d1c2p2  42158  hashscontpow  42161  rspcsbnea  42170  aks6d1c6lem3  42211  fsuppind  42629  zindbi  42985  cnvtrucl0  43663  ismnushort  44340  e2ebind  44602  uunT1  44818  ovnval2  46589  ovnval2b  46596  hoiqssbl  46669  6gbe  47808  8gbe  47810  isgrim  47919  usgrexmpl1tri  48062  gpgov  48079  gpg3kgrtriex  48126