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  1437  3anbi13d  1438  3anbi23d  1439  3anbi1d  1440  3anbi2d  1441  3anbi3d  1442  nfald2  2453  exdistrf  2455  sb6x  2472  axc16gALT  2498  raleqOLD  3348  rexeqOLD  3349  vtoclegft  3601  ralxpxfr2d  3659  rr19.3v  3680  rr19.28v  3681  rabtru  3705  moeq3  3734  euxfr2w  3742  euxfr2  3744  reuxfrd  3770  dfif3  4562  sseliALT  5327  copsexgw  5510  copsexg  5511  soeq1  5629  frd  5656  soinxp  5781  idrefALT  6143  ordtri3or  6427  nfriotadw  7412  oprabidw  7479  ov6g  7614  ovg  7615  sorpssi  7764  dfxp3  8102  fsplit  8158  frxp3  8192  xpord3inddlem  8195  aceq1  10186  aceq2  10188  axpowndlem4  10669  axpownd  10670  ltsopr  11101  creur  12287  creui  12288  o1fsum  15861  sumodd  16436  sadfval  16498  sadcp1  16501  pceu  16893  vdwlem12  17039  sgrp2rid2ex  18962  gsumval3eu  19946  lss1d  20984  nrmr0reg  23778  stdbdxmet  24549  xrsxmet  24850  cmetcaulem  25341  bcth3  25384  iundisj2  25603  ulmdvlem3  26463  ulmdv  26464  dchrvmasumlem2  27560  colrot1  28585  lnrot1  28649  lnrot2  28650  wlkson  29692  trlsfval  29731  pthsfval  29757  spthsfval  29758  clwlks  29808  crcts  29824  cycls  29825  3cyclfrgrrn1  30317  frgrwopreg  30355  reuxfrdf  32519  iundisj2f  32612  iundisj2fi  32802  ordtprsuni  33865  pmeasmono  34289  erdszelem9  35167  satfv1fvfmla1  35391  opnrebl2  36287  wl-ifpimpr  37432  wl-df-3xor  37434  wl-ax11-lem9  37547  ax12fromc15  38861  axc16g-o  38890  ax12indalem  38901  ax12inda2ALT  38902  dihopelvalcpre  41205  lpolconN  41444  dvrelog2b  42023  isprimroot  42050  aks6d1c2p2  42076  hashscontpow  42079  rspcsbnea  42088  aks6d1c6lem3  42129  fsuppind  42545  zindbi  42903  cnvtrucl0  43586  ismnushort  44270  e2ebind  44534  uunT1  44751  ovnval2  46466  ovnval2b  46473  hoiqssbl  46546  6gbe  47645  8gbe  47647  isgrim  47752  usgrexmpl1tri  47840