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  1397  3anbi13d  1398  3anbi23d  1399  3anbi1d  1400  3anbi2d  1401  3anbi3d  1402  nfald2  2330  exdistrf  2332  ax12OLD  2340  axc16gALT  2366  sb6x  2383  ralxpxfr2d  3316  rr19.3v  3333  rr19.28v  3334  rabtru  3349  moeq3  3370  euxfr2  3378  dfif3  4078  sseliALT  4761  reuxfr2d  4861  copsexg  4926  soeq1  5024  soinxp  5154  ordtri3or  5724  ov6g  6763  ovg  6764  sorpssi  6908  dfxp3  7190  aceq1  8900  aceq2  8902  axpowndlem4  9382  axpownd  9383  ltsopr  9814  creur  10974  creui  10975  o1fsum  14491  sumodd  15054  sadfval  15117  sadcp1  15120  pceu  15494  vdwlem12  15639  sgrp2rid2ex  17354  gsumval3eu  18245  lss1d  18903  nrmr0reg  21492  stdbdxmet  22260  xrsxmet  22552  cmetcaulem  23026  bcth3  23068  iundisj2  23257  ulmdvlem3  24094  ulmdv  24095  dchrvmasumlem2  25121  colrot1  25388  lnrot1  25452  lnrot2  25453  dfcgra2  25655  isinag  25663  isrusgr  26361  wksfval  26409  wlkson  26455  trlsfval  26495  pthsfval  26520  spthsfval  26521  clwlks  26571  crcts  26586  cycls  26587  3cyclfrgrrn1  27047  frgrregorufr0  27081  reuxfr3d  29218  iundisj2f  29289  iundisj2fi  29439  ordtprsuni  29789  isrnsigaOLD  29998  pmeasmono  30209  erdszelem9  30942  opnrebl2  32011  wl-ax11-lem9  33041  ax12fromc15  33709  axc16g-o  33738  ax12indalem  33749  ax12inda2ALT  33750  dihopelvalcpre  36056  lpolconN  36295  zindbi  37030  cnvtrucl0  37451  e2ebind  38300  uunT1  38528  trsbcVD  38635  ovnval2  40096  ovnval2b  40103  hoiqssbl  40176  6gbe  40984  8gbe  40986