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  2480  exdistrf  2482  sb6x  2499  axc16gALT  2525  vtoclegft  3551  ralxpxfr2d  3608  rr19.3v  3629  rr19.28v  3630  rabtru  3651  moeq3  3678  euxfr2w  3686  euxfr2  3688  reuxfrd  3714  vn0  4301  vn0OLD  4302  eq0  4307  ab0orv  4342  dfif3  4507  sseliALT  5277  copsexgwOLD  5478  copsexg  5479  soeq1  5595  frd  5623  soinxp  5748  idrefALT  6118  ordtri3or  6400  nfriotadw  7388  oprabidw  7454  ov6g  7587  ovg  7588  sorpssi  7739  dfxp3  8067  fsplit  8121  frxp3  8156  xpord3inddlem  8159  aceq1  10120  aceq2  10122  axpowndlem4  10603  axpownd  10604  ltsopr  11035  creur  12230  creui  12231  o1fsum  15891  sumodd  16471  sadfval  16535  sadcp1  16538  pceu  16931  vdwlem12  17077  sgrp2rid2ex  19020  gsumval3eu  20005  lss1d  21121  nrmr0reg  23943  stdbdxmet  24709  xrsxmet  25004  cmetcaulem  25484  bcth3  25527  iundisj2  25745  ulmdvlem3  26602  ulmdv  26603  dchrvmasumlem2  27699  colrot1  28865  lnrot1  28933  lnrot2  28934  tgplnfn  29094  plngval  29096  isplng  29097  wlkson  30041  trlsfval  30080  pthsfval  30105  spthsfval  30106  clwlks  30158  crcts  30174  cycls  30175  3cyclfrgrrn1  30673  frgrwopreg  30711  reuxfrdf  32874  iundisj2f  32972  iundisj2fi  33179  constrcbvlem  34176  ordtprsuni  34340  pmeasmono  34746  erdszelem9  35712  satfv1fvfmla1  35936  opnrebl2  36873  wl-ifpimpr  38153  wl-df-3xor  38155  ax12fromc15  39720  axc16g-o  39749  ax12indalem  39760  ax12inda2ALT  39761  dihopelvalcpre  42063  lpolconN  42302  dvrelog2b  42874  isprimroot  42901  aks6d1c2p2  42927  hashscontpow  42930  rspcsbnea  42939  aks6d1c6lem3  42980  fsuppind  43363  zindbi  43714  cnvtrucl0  44391  ismnushort  45052  e2ebind  45313  uunT1  45529  ovnval2  47300  ovnval2b  47307  hoiqssbl  47380  6gbe  48577  8gbe  48579  isgrim  48688  usgrexmpl1tri  48831  gpgov  48848  gpg3kgrtriex  48895