Theorem biidd 252

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 251	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3anbi12d  1440  3anbi13d  1441  3anbi23d  1442  3anbi1d  1443  3anbi2d  1444  3anbi3d  1445  nfald2  2362  exdistrf  2364  ax12OLD  2372  axc16gALT  2395  sb6x  2412  ralxpxfr2d  3358  rr19.3v  3377  rr19.28v  3378  rabtru  3393  moeq3  3416  euxfr2  3424  dfif3  4133  sseliALT  4824  reuxfr2d  4921  copsexg  4985  soeq1  5083  soinxp  5217  ordtri3or  5793  ov6g  6840  ovg  6841  sorpssi  6985  dfxp3  7275  aceq1  8978  aceq2  8980  axpowndlem4  9460  axpownd  9461  ltsopr  9892  creur  11052  creui  11053  o1fsum  14589  sumodd  15158  sadfval  15221  sadcp1  15224  pceu  15598  vdwlem12  15743  sgrp2rid2ex  17461  gsumval3eu  18351  lss1d  19011  nrmr0reg  21600  stdbdxmet  22367  xrsxmet  22659  cmetcaulem  23132  bcth3  23174  iundisj2  23363  ulmdvlem3  24201  ulmdv  24202  dchrvmasumlem2  25232  colrot1  25499  lnrot1  25563  lnrot2  25564  dfcgra2  25766  isinag  25774  isrusgr  26513  wksfval  26561  wlkson  26608  trlsfval  26648  pthsfval  26673  spthsfval  26674  clwlks  26724  crcts  26739  cycls  26740  3cyclfrgrrn1  27265  frgrwopreg  27303  reuxfr3d  29456  iundisj2f  29529  iundisj2fi  29684  ordtprsuni  30093  isrnsigaOLD  30303  pmeasmono  30514  erdszelem9  31307  opnrebl2  32441  wl-ax11-lem9  33500  ax12fromc15  34509  axc16g-o  34538  ax12indalem  34549  ax12inda2ALT  34550  dihopelvalcpre  36854  lpolconN  37093  zindbi  37828  cnvtrucl0  38248  e2ebind  39096  uunT1  39324  trsbcVD  39427  ovnval2  41080  ovnval2b  41087  hoiqssbl  41160  6gbe  41984  8gbe  41986