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  1549  3anbi13d  1550  3anbi23d  1551  3anbi1d  1552  3anbi2d  1553  3anbi3d  1554  nfald2  2471  exdistrf  2473  ax12OLD  2481  axc16gALT  2504  sb6x  2521  ralxpxfr2d  3466  rr19.3v  3485  rr19.28v  3486  rabtru  3501  moeq3  3524  euxfr2  3532  dfif3  4244  sseliALT  4943  reuxfr2d  5040  copsexg  5104  soeq1  5206  soinxp  5340  ordtri3or  5916  ov6g  6964  ovg  6965  sorpssi  7109  dfxp3  7399  aceq1  9150  aceq2  9152  axpowndlem4  9634  axpownd  9635  ltsopr  10066  creur  11226  creui  11227  o1fsum  14764  sumodd  15333  sadfval  15396  sadcp1  15399  pceu  15773  vdwlem12  15918  sgrp2rid2ex  17635  gsumval3eu  18525  lss1d  19185  nrmr0reg  21774  stdbdxmet  22541  xrsxmet  22833  cmetcaulem  23306  bcth3  23348  iundisj2  23537  ulmdvlem3  24375  ulmdv  24376  dchrvmasumlem2  25407  colrot1  25674  lnrot1  25738  lnrot2  25739  dfcgra2  25941  isinag  25949  isrusgr  26688  wksfval  26736  wlkson  26783  trlsfval  26823  pthsfval  26848  spthsfval  26849  clwlks  26899  crcts  26915  cycls  26916  3cyclfrgrrn1  27460  frgrwopreg  27498  reuxfr3d  29658  iundisj2f  29731  iundisj2fi  29886  ordtprsuni  30295  isrnsigaOLD  30505  pmeasmono  30716  erdszelem9  31509  opnrebl2  32643  wl-ax11-lem9  33701  ax12fromc15  34712  axc16g-o  34741  ax12indalem  34752  ax12inda2ALT  34753  dihopelvalcpre  37057  lpolconN  37296  zindbi  38031  cnvtrucl0  38451  e2ebind  39299  uunT1  39527  trsbcVD  39630  ovnval2  41283  ovnval2b  41290  hoiqssbl  41363  6gbe  42187  8gbe  42189