MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biidd Structured version   Visualization version   GIF version

Theorem biidd 265
Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
Assertion
Ref Expression
biidd (𝜑 → (𝜓𝜓))

Proof of Theorem biidd
StepHypRef Expression
1 biid 264 . 2 (𝜓𝜓)
21a1i 11 1 (𝜑 → (𝜓𝜓))
Colors of variables: wff setvar class
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  1077  3anbi12d  1434  3anbi13d  1435  3anbi23d  1436  3anbi1d  1437  3anbi2d  1438  3anbi3d  1439  nfald2  2459  exdistrf  2461  sb6x  2479  axc16gALT  2511  raleq  3361  rexeq  3362  ralxpxfr2d  3590  rr19.3v  3610  rr19.28v  3611  rabtru  3628  moeq3  3654  euxfr2w  3662  euxfr2  3664  reuxfrd  3690  dfif3  4442  sseliALT  5180  copsexgw  5349  copsexg  5350  soeq1  5462  soinxp  5601  idrefALT  5944  ordtri3or  6195  nfriotadw  7105  oprabidw  7170  ov6g  7296  ovg  7297  sorpssi  7439  dfxp3  7745  fsplit  7799  aceq1  9532  aceq2  9534  axpowndlem4  10015  axpownd  10016  ltsopr  10447  creur  11623  creui  11624  o1fsum  15163  sumodd  15732  sadfval  15794  sadcp1  15797  pceu  16176  vdwlem12  16321  sgrp2rid2ex  18087  gsumval3eu  19020  lss1d  19731  nrmr0reg  22357  stdbdxmet  23125  xrsxmet  23417  cmetcaulem  23895  bcth3  23938  iundisj2  24156  ulmdvlem3  25000  ulmdv  25001  dchrvmasumlem2  26085  colrot1  26356  lnrot1  26420  lnrot2  26421  wlkson  27449  trlsfval  27488  pthsfval  27513  spthsfval  27514  clwlks  27564  crcts  27580  cycls  27581  3cyclfrgrrn1  28073  frgrwopreg  28111  reuxfrdf  30265  iundisj2f  30356  iundisj2fi  30549  ordtprsuni  31270  pmeasmono  31690  erdszelem9  32554  satfv1fvfmla1  32778  opnrebl2  33777  wl-ifpimpr  34876  wl-df-3xor  34878  wl-ax11-lem9  34983  ax12fromc15  36194  axc16g-o  36223  ax12indalem  36234  ax12inda2ALT  36235  dihopelvalcpre  38537  lpolconN  38776  fsuppind  39443  zindbi  39874  cnvtrucl0  40311  e2ebind  41256  uunT1  41473  ovnval2  43171  ovnval2b  43178  hoiqssbl  43251  6gbe  44276  8gbe  44278
  Copyright terms: Public domain W3C validator