Theorem biidd 264

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3anbi12d  1433  3anbi13d  1434  3anbi23d  1435  3anbi1d  1436  3anbi2d  1437  3anbi3d  1438  nfald2  2467  exdistrf  2469  sb6x  2487  axc16gALT  2529  raleq  3407  rexeq  3408  ralxpxfr2d  3641  rr19.3v  3663  rr19.28v  3664  rabtru  3679  moeq3  3705  euxfr2w  3713  euxfr2  3715  reuxfrd  3741  dfif3  4483  sseliALT  5215  copsexgw  5383  copsexg  5384  soeq1  5496  soinxp  5635  idrefALT  5975  ordtri3or  6225  nfriotadw  7124  oprabidw  7189  ov6g  7314  ovg  7315  sorpssi  7457  dfxp3  7761  fsplit  7814  aceq1  9545  aceq2  9547  axpowndlem4  10024  axpownd  10025  ltsopr  10456  creur  11634  creui  11635  o1fsum  15170  sumodd  15741  sadfval  15803  sadcp1  15806  pceu  16185  vdwlem12  16330  sgrp2rid2ex  18094  gsumval3eu  19026  lss1d  19737  nrmr0reg  22359  stdbdxmet  23127  xrsxmet  23419  cmetcaulem  23893  bcth3  23936  iundisj2  24152  ulmdvlem3  24992  ulmdv  24993  dchrvmasumlem2  26076  colrot1  26347  lnrot1  26411  lnrot2  26412  wksfval  27393  wlkson  27440  trlsfval  27479  pthsfval  27504  spthsfval  27505  clwlks  27555  crcts  27571  cycls  27572  3cyclfrgrrn1  28066  frgrwopreg  28104  reuxfrdf  30257  iundisj2f  30342  iundisj2fi  30522  ordtprsuni  31164  pmeasmono  31584  subgrwlk  32381  erdszelem9  32448  satfv1fvfmla1  32672  opnrebl2  33671  bj-ififc  33917  wl-ax11-lem9  34827  ax12fromc15  36043  axc16g-o  36072  ax12indalem  36083  ax12inda2ALT  36084  dihopelvalcpre  38386  lpolconN  38625  zindbi  39550  cnvtrucl0  39991  e2ebind  40904  uunT1  41121  ovnval2  42834  ovnval2b  42841  hoiqssbl  42914  6gbe  43943  8gbe  43945