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  1096  3anbi12d  1465  3anbi13d  1466  3anbi23d  1467  3anbi1d  1468  3anbi2d  1469  3anbi3d  1470  nfald2  2475  exdistrf  2477  sb6x  2494  axc16gALT  2520  vtoclegft  3544  ralxpxfr2d  3600  rr19.3v  3621  rr19.28v  3622  rabtru  3643  moeq3  3670  euxfr2w  3678  euxfr2  3680  reuxfrd  3706  vn0  4291  vn0OLD  4292  eq0  4297  ab0orv  4332  dfif3  4497  sseliALT  5263  copsexgwOLD  5461  copsexg  5462  soeq1  5580  frd  5608  soinxp  5733  idrefALT  6105  ordtri3or  6388  nfriotadw  7377  oprabidw  7443  ov6g  7576  ovg  7577  sorpssi  7734  dfxp3  8061  fsplit  8117  frxp3  8152  xpord3inddlem  8155  aceq1  10177  aceq2  10179  axpowndlem4  10666  axpownd  10667  ltsopr  11098  creur  12295  creui  12296  o1fsum  15960  sumodd  16538  sadfval  16602  sadcp1  16605  pceu  17004  vdwlem12  17150  sgrp2rid2ex  19106  gsumval3eu  20098  lss1d  21218  nrmr0reg  24048  stdbdxmet  24814  xrsxmet  25109  cmetcaulem  25589  bcth3  25632  iundisj2  25850  ulmdvlem3  26711  ulmdv  26712  dchrvmasumlem2  27807  colrot1  29004  lnrot1  29073  lnrot2  29074  tgplnfn  29235  plngval  29237  isplng  29238  elcgrabasi  29357  wlkson  30217  trlsfval  30260  pthsfval  30286  spthsfval  30287  clwlks  30341  crcts  30357  cycls  30358  3cyclfrgrrn1  30868  frgrwopreg  30906  reuxfrdf  33069  iundisj2f  33166  iundisj2fi  33371  constrcbvlem  34369  ordtprsuni  34533  pmeasmono  34939  erdszelem9  35933  satfv1fvfmla1  36157  opnrebl2  37079  wl-ifpimpr  38357  wl-df-3xor  38359  ax12fromc15  39930  axc16g-o  39959  ax12indalem  39970  ax12inda2ALT  39971  dihopelvalcpre  42273  lpolconN  42512  dvrelog2b  43084  isprimroot  43111  aks6d1c2p2  43137  hashscontpow  43140  rspcsbnea  43149  aks6d1c6lem3  43190  fsuppind  43580  zindbi  43906  cnvtrucl0  44583  ismnushort  45244  e2ebind  45505  uunT1  45721  ovnval2  47499  ovnval2b  47506  hoiqssbl  47579  6gbe  48813  8gbe  48815  isgrim  48924  usgrexmpl1tri  49067  gpgov  49084  gpg3kgrtriex  49131