Theorem biidd 261

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ifpbi23d  1079  3anbi12d  1436  3anbi13d  1437  3anbi23d  1438  3anbi1d  1439  3anbi2d  1440  3anbi3d  1441  nfald2  2445  exdistrf  2447  sb6x  2464  axc16gALT  2494  raleq  3342  rexeq  3343  ralxpxfr2d  3576  rr19.3v  3598  rr19.28v  3599  rabtru  3621  moeq3  3647  euxfr2w  3655  euxfr2  3657  reuxfrd  3683  dfif3  4473  sseliALT  5233  copsexgw  5404  copsexg  5405  soeq1  5524  frd  5548  soinxp  5668  idrefALT  6018  ordtri3or  6298  nfriotadw  7240  oprabidw  7306  ov6g  7436  ovg  7437  sorpssi  7582  dfxp3  7901  fsplit  7957  aceq1  9873  aceq2  9875  axpowndlem4  10356  axpownd  10357  ltsopr  10788  creur  11967  creui  11968  o1fsum  15525  sumodd  16097  sadfval  16159  sadcp1  16162  pceu  16547  vdwlem12  16693  sgrp2rid2ex  18566  gsumval3eu  19505  lss1d  20225  nrmr0reg  22900  stdbdxmet  23671  xrsxmet  23972  cmetcaulem  24452  bcth3  24495  iundisj2  24713  ulmdvlem3  25561  ulmdv  25562  dchrvmasumlem2  26646  colrot1  26920  lnrot1  26984  lnrot2  26985  wlkson  28024  trlsfval  28063  pthsfval  28089  spthsfval  28090  clwlks  28140  crcts  28156  cycls  28157  3cyclfrgrrn1  28649  frgrwopreg  28687  reuxfrdf  30839  iundisj2f  30929  iundisj2fi  31118  ordtprsuni  31869  pmeasmono  32291  erdszelem9  33161  satfv1fvfmla1  33385  xpord3ind  33800  opnrebl2  34510  wl-ifpimpr  35637  wl-df-3xor  35639  wl-ax11-lem9  35744  ax12fromc15  36919  axc16g-o  36948  ax12indalem  36959  ax12inda2ALT  36960  dihopelvalcpre  39262  lpolconN  39501  dvrelog2b  40074  sticksstones11  40112  fsuppind  40279  zindbi  40768  cnvtrucl0  41232  ismnushort  41919  e2ebind  42183  uunT1  42400  ovnval2  44083  ovnval2b  44090  hoiqssbl  44163  6gbe  45223  8gbe  45225