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 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ifpbi23d  1095  3anbi12d  1464  3anbi13d  1465  3anbi23d  1466  3anbi1d  1467  3anbi2d  1468  3anbi3d  1469  nfald2  2476  exdistrf  2478  sb6x  2495  axc16gALT  2521  vtoclegft  3547  ralxpxfr2d  3604  rr19.3v  3625  rr19.28v  3626  rabtru  3647  moeq3  3674  euxfr2w  3682  euxfr2  3684  reuxfrd  3710  vn0  4297  vn0OLD  4298  eq0  4303  ab0orv  4338  dfif3  4501  sseliALT  5271  copsexgwOLD  5472  copsexg  5473  soeq1  5589  frd  5617  soinxp  5742  idrefALT  6112  ordtri3or  6393  nfriotadw  7377  oprabidw  7443  ov6g  7576  ovg  7577  sorpssi  7728  dfxp3  8056  fsplit  8110  frxp3  8145  xpord3inddlem  8148  aceq1  10108  aceq2  10110  axpowndlem4  10591  axpownd  10592  ltsopr  11023  creur  12218  creui  12219  o1fsum  15872  sumodd  16452  sadfval  16516  sadcp1  16519  pceu  16912  vdwlem12  17058  sgrp2rid2ex  18995  gsumval3eu  19980  lss1d  21095  nrmr0reg  23917  stdbdxmet  24683  xrsxmet  24978  cmetcaulem  25458  bcth3  25501  iundisj2  25719  ulmdvlem3  26576  ulmdv  26577  dchrvmasumlem2  27673  colrot1  28839  lnrot1  28907  lnrot2  28908  tgplnfn  29068  plngval  29070  isplng  29071  wlkson  30015  trlsfval  30054  pthsfval  30079  spthsfval  30080  clwlks  30132  crcts  30148  cycls  30149  3cyclfrgrrn1  30647  frgrwopreg  30685  reuxfrdf  32848  iundisj2f  32946  iundisj2fi  33153  constrcbvlem  34154  ordtprsuni  34318  pmeasmono  34723  erdszelem9  35699  satfv1fvfmla1  35923  opnrebl2  36860  wl-ifpimpr  38140  wl-df-3xor  38142  ax12fromc15  39707  axc16g-o  39736  ax12indalem  39747  ax12inda2ALT  39748  dihopelvalcpre  42050  lpolconN  42289  dvrelog2b  42861  isprimroot  42888  aks6d1c2p2  42914  hashscontpow  42917  rspcsbnea  42926  aks6d1c6lem3  42967  fsuppind  43350  zindbi  43701  cnvtrucl0  44378  ismnushort  45039  e2ebind  45300  uunT1  45516  ovnval2  47287  ovnval2b  47294  hoiqssbl  47367  6gbe  48564  8gbe  48566  isgrim  48675  usgrexmpl1tri  48818  gpgov  48835  gpg3kgrtriex  48882