Theorem biidd 265

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ifpbi23d  1096  3anbi12d  1465  3anbi13d  1466  3anbi23d  1467  3anbi1d  1468  3anbi2d  1469  3anbi3d  1470  nfald2  2477  exdistrf  2479  sb6x  2496  axc16gALT  2522  vtoclegft  3549  ralxpxfr2d  3606  rr19.3v  3627  rr19.28v  3628  rabtru  3649  moeq3  3676  euxfr2w  3684  euxfr2  3686  reuxfrd  3712  vn0  4299  vn0OLD  4300  eq0  4305  ab0orv  4340  dfif3  4503  sseliALT  5273  copsexgwOLD  5475  copsexg  5476  soeq1  5592  frd  5620  soinxp  5745  idrefALT  6115  ordtri3or  6395  nfriotadw  7377  oprabidw  7443  ov6g  7576  ovg  7577  sorpssi  7728  dfxp3  8059  fsplit  8113  frxp3  8148  xpord3inddlem  8151  aceq1  10102  aceq2  10104  axpowndlem4  10586  axpownd  10587  ltsopr  11018  creur  12213  creui  12214  o1fsum  15867  sumodd  16447  sadfval  16511  sadcp1  16514  pceu  16907  vdwlem12  17053  sgrp2rid2ex  18990  gsumval3eu  19975  lss1d  21065  nrmr0reg  23887  stdbdxmet  24653  xrsxmet  24948  cmetcaulem  25428  bcth3  25471  iundisj2  25689  ulmdvlem3  26546  ulmdv  26547  dchrvmasumlem2  27643  colrot1  28809  lnrot1  28877  lnrot2  28878  tgplnfn  29038  plngval  29040  isplng  29041  wlkson  29985  trlsfval  30024  pthsfval  30049  spthsfval  30050  clwlks  30102  crcts  30118  cycls  30119  3cyclfrgrrn1  30617  frgrwopreg  30655  reuxfrdf  32818  iundisj2f  32916  iundisj2fi  33123  constrcbvlem  34126  ordtprsuni  34290  pmeasmono  34695  erdszelem9  35672  satfv1fvfmla1  35896  opnrebl2  36813  wl-ifpimpr  38093  wl-df-3xor  38095  ax12fromc15  39660  axc16g-o  39689  ax12indalem  39700  ax12inda2ALT  39701  dihopelvalcpre  42003  lpolconN  42242  dvrelog2b  42814  isprimroot  42841  aks6d1c2p2  42867  hashscontpow  42870  rspcsbnea  42879  aks6d1c6lem3  42920  fsuppind  43305  zindbi  43656  cnvtrucl0  44333  ismnushort  44994  e2ebind  45255  uunT1  45471  ovnval2  47242  ovnval2b  47249  hoiqssbl  47322  6gbe  48519  8gbe  48521  isgrim  48630  usgrexmpl1tri  48773  gpgov  48790  gpg3kgrtriex  48837