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  1094  3anbi12d  1461  3anbi13d  1462  3anbi23d  1463  3anbi1d  1464  3anbi2d  1465  3anbi3d  1466  nfald2  2479  exdistrf  2481  sb6x  2498  axc16gALT  2524  vtoclegft  3551  ralxpxfr2d  3608  rr19.3v  3629  rr19.28v  3630  rabtru  3651  moeq3  3678  euxfr2w  3686  euxfr2  3688  reuxfrd  3714  vn0  4300  eq0  4305  ab0orv  4339  dfif3  4498  sseliALT  5263  copsexgwOLD  5463  copsexg  5464  soeq1  5580  frd  5608  soinxp  5733  idrefALT  6103  ordtri3or  6382  nfriotadw  7365  oprabidw  7431  ov6g  7564  ovg  7565  sorpssi  7716  dfxp3  8046  fsplit  8100  frxp3  8135  xpord3inddlem  8138  aceq1  10089  aceq2  10091  axpowndlem4  10573  axpownd  10574  ltsopr  11005  creur  12200  creui  12201  o1fsum  15853  sumodd  16434  sadfval  16498  sadcp1  16501  pceu  16894  vdwlem12  17040  sgrp2rid2ex  18977  gsumval3eu  19962  lss1d  21050  nrmr0reg  23863  stdbdxmet  24629  xrsxmet  24924  cmetcaulem  25404  bcth3  25447  iundisj2  25665  ulmdvlem3  26519  ulmdv  26520  dchrvmasumlem2  27616  colrot1  28782  lnrot1  28846  lnrot2  28847  tgplnfn  29001  plngval  29003  isplng  29004  wlkson  29909  trlsfval  29948  pthsfval  29973  spthsfval  29974  clwlks  30026  crcts  30042  cycls  30043  3cyclfrgrrn1  30541  frgrwopreg  30579  reuxfrdf  32743  iundisj2f  32841  iundisj2fi  33050  constrcbvlem  34057  ordtprsuni  34221  pmeasmono  34626  erdszelem9  35557  satfv1fvfmla1  35781  opnrebl2  36689  wl-ifpimpr  37967  wl-df-3xor  37969  ax12fromc15  39536  axc16g-o  39565  ax12indalem  39576  ax12inda2ALT  39577  dihopelvalcpre  41879  lpolconN  42118  dvrelog2b  42690  isprimroot  42717  aks6d1c2p2  42743  hashscontpow  42746  rspcsbnea  42755  aks6d1c6lem3  42796  fsuppind  43179  zindbi  43530  cnvtrucl0  44207  ismnushort  44870  e2ebind  45131  uunT1  45347  ovnval2  47118  ovnval2b  47125  hoiqssbl  47198  6gbe  48392  8gbe  48394  isgrim  48503  usgrexmpl1tri  48646  gpgov  48663  gpg3kgrtriex  48710