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:  ifpbi23d  1090  3anbi12d  1457  3anbi13d  1458  3anbi23d  1459  3anbi1d  1460  3anbi2d  1461  3anbi3d  1462  nfald2  2475  exdistrf  2477  sb6x  2494  axc16gALT  2520  vtoclegft  3547  ralxpxfr2d  3604  rr19.3v  3625  rr19.28v  3626  rabtru  3647  moeq3  3673  euxfr2w  3681  euxfr2  3683  reuxfrd  3709  vn0  4295  eq0  4300  ab0orv  4333  dfif3  4492  sseliALT  5256  copsexgwOLD  5456  copsexg  5457  soeq1  5572  frd  5600  soinxp  5725  idrefALT  6095  ordtri3or  6372  nfriotadw  7355  oprabidw  7421  ov6g  7554  ovg  7555  sorpssi  7706  dfxp3  8036  fsplit  8089  frxp3  8124  xpord3inddlem  8127  aceq1  10066  aceq2  10068  axpowndlem4  10551  axpownd  10552  ltsopr  10983  creur  12182  creui  12183  o1fsum  15831  sumodd  16412  sadfval  16476  sadcp1  16479  pceu  16872  vdwlem12  17018  sgrp2rid2ex  18954  gsumval3eu  19934  lss1d  21017  nrmr0reg  23796  stdbdxmet  24562  xrsxmet  24857  cmetcaulem  25337  bcth3  25380  iundisj2  25598  ulmdvlem3  26452  ulmdv  26453  dchrvmasumlem2  27549  colrot1  28715  lnrot1  28779  lnrot2  28780  wlkson  29811  trlsfval  29850  pthsfval  29875  spthsfval  29876  clwlks  29928  crcts  29944  cycls  29945  3cyclfrgrrn1  30443  frgrwopreg  30481  reuxfrdf  32648  iundisj2f  32749  iundisj2fi  32959  constrcbvlem  34012  ordtprsuni  34176  pmeasmono  34581  erdszelem9  35509  satfv1fvfmla1  35733  opnrebl2  36641  wl-ifpimpr  37920  wl-df-3xor  37922  ax12fromc15  39489  axc16g-o  39518  ax12indalem  39529  ax12inda2ALT  39530  dihopelvalcpre  41832  lpolconN  42071  dvrelog2b  42643  isprimroot  42670  aks6d1c2p2  42696  hashscontpow  42699  rspcsbnea  42708  aks6d1c6lem3  42749  fsuppind  43132  zindbi  43483  cnvtrucl0  44160  ismnushort  44837  e2ebind  45099  uunT1  45315  ovnval2  47079  ovnval2b  47086  hoiqssbl  47159  6gbe  48353  8gbe  48355  isgrim  48464  usgrexmpl1tri  48607  gpgov  48624  gpg3kgrtriex  48671