Theorem biidd 254

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3anbi12d  1416  3anbi13d  1417  3anbi23d  1418  3anbi1d  1419  3anbi2d  1420  3anbi3d  1421  nfald2  2381  exdistrf  2383  sb6x  2402  axc16gALT  2450  raleq  3346  rexeq  3347  ralxpxfr2d  3555  rr19.3v  3576  rr19.28v  3577  rabtru  3593  moeq3  3618  euxfr2  3626  reuxfr3d  3652  dfif3  4364  sseliALT  5070  copsexg  5238  soeq1  5346  soinxp  5483  idrefALT  5813  ordtri3or  6061  ov6g  7128  ovg  7129  sorpssi  7273  dfxp3  7567  aceq1  9337  aceq2  9339  axpowndlem4  9820  axpownd  9821  ltsopr  10252  creur  11433  creui  11434  o1fsum  15028  sumodd  15599  sadfval  15661  sadcp1  15664  pceu  16039  vdwlem12  16184  sgrp2rid2ex  17883  gsumval3eu  18778  lss1d  19457  nrmr0reg  22061  stdbdxmet  22828  xrsxmet  23120  cmetcaulem  23594  bcth3  23637  iundisj2  23853  ulmdvlem3  24693  ulmdv  24694  dchrvmasumlem2  25776  colrot1  26047  lnrot1  26111  lnrot2  26112  wksfval  27094  wlkson  27140  trlsfval  27183  pthsfval  27210  spthsfval  27211  clwlks  27261  crcts  27277  cycls  27278  3cyclfrgrrn1  27819  frgrwopreg  27857  iundisj2f  30106  iundisj2fi  30269  ordtprsuni  30803  isrnsigaOLD  31013  pmeasmono  31224  erdszelem9  32028  opnrebl2  33187  wl-ax11-lem9  34263  ax12fromc15  35483  axc16g-o  35512  ax12indalem  35523  ax12inda2ALT  35524  dihopelvalcpre  37826  lpolconN  38065  zindbi  38936  cnvtrucl0  39344  e2ebind  40313  uunT1  40530  ovnval2  42256  ovnval2b  42263  hoiqssbl  42336  6gbe  43302  8gbe  43304