Theorem biidd 262

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ifpbi23d  1080  3anbi12d  1440  3anbi13d  1441  3anbi23d  1442  3anbi1d  1443  3anbi2d  1444  3anbi3d  1445  nfald2  2449  exdistrf  2451  sb6x  2468  axc16gALT  2494  vtoclegft  3531  ralxpxfr2d  3588  rr19.3v  3609  rr19.28v  3610  rabtru  3632  moeq3  3658  euxfr2w  3666  euxfr2  3668  reuxfrd  3694  vn0  4285  eq0  4290  ab0orv  4323  dfif3  4481  sseliALT  5244  copsexgwOLD  5444  copsexg  5445  soeq1  5560  frd  5588  soinxp  5713  idrefALT  6076  ordtri3or  6355  nfriotadw  7332  oprabidw  7398  ov6g  7531  ovg  7532  sorpssi  7683  dfxp3  8014  fsplit  8067  frxp3  8101  xpord3inddlem  8104  aceq1  10039  aceq2  10041  axpowndlem4  10523  axpownd  10524  ltsopr  10955  creur  12153  creui  12154  o1fsum  15776  sumodd  16357  sadfval  16421  sadcp1  16424  pceu  16817  vdwlem12  16963  sgrp2rid2ex  18898  gsumval3eu  19879  lss1d  20958  nrmr0reg  23714  stdbdxmet  24480  xrsxmet  24775  cmetcaulem  25255  bcth3  25298  iundisj2  25516  ulmdvlem3  26367  ulmdv  26368  dchrvmasumlem2  27461  colrot1  28627  lnrot1  28691  lnrot2  28692  wlkson  29723  trlsfval  29762  pthsfval  29787  spthsfval  29788  clwlks  29840  crcts  29856  cycls  29857  3cyclfrgrrn1  30355  frgrwopreg  30393  reuxfrdf  32560  iundisj2f  32660  iundisj2fi  32870  constrcbvlem  33899  ordtprsuni  34063  pmeasmono  34468  erdszelem9  35381  satfv1fvfmla1  35605  opnrebl2  36503  wl-ifpimpr  37782  wl-df-3xor  37784  ax12fromc15  39351  axc16g-o  39380  ax12indalem  39391  ax12inda2ALT  39392  dihopelvalcpre  41694  lpolconN  41933  dvrelog2b  42505  isprimroot  42532  aks6d1c2p2  42558  hashscontpow  42561  rspcsbnea  42570  aks6d1c6lem3  42611  fsuppind  43023  zindbi  43374  cnvtrucl0  44051  ismnushort  44728  e2ebind  44990  uunT1  45206  ovnval2  46973  ovnval2b  46980  hoiqssbl  47053  6gbe  48247  8gbe  48249  isgrim  48358  usgrexmpl1tri  48501  gpgov  48518  gpg3kgrtriex  48565