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

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

Proof of Theorem biidd
StepHypRef Expression
1 biid 261 . 2 (𝜓𝜓)
21a1i 11 1 (𝜑 → (𝜓𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  ifpbi23d  1081  3anbi12d  1438  3anbi13d  1439  3anbi23d  1440  3anbi1d  1441  3anbi2d  1442  3anbi3d  1443  nfald2  2444  exdistrf  2446  sb6x  2463  axc16gALT  2489  raleq  3308  rexeq  3309  vtoclegft  3541  ralxpxfr2d  3597  rr19.3v  3620  rr19.28v  3621  rabtru  3643  moeq3  3671  euxfr2w  3679  euxfr2  3681  reuxfrd  3707  dfif3  4501  sseliALT  5267  copsexgw  5448  copsexg  5449  soeq1  5567  frd  5593  soinxp  5714  idrefALT  6066  ordtri3or  6350  nfriotadw  7322  oprabidw  7389  ov6g  7519  ovg  7520  sorpssi  7667  dfxp3  7994  fsplit  8050  frxp3  8084  xpord3inddlem  8087  aceq1  10058  aceq2  10060  axpowndlem4  10541  axpownd  10542  ltsopr  10973  creur  12152  creui  12153  o1fsum  15703  sumodd  16275  sadfval  16337  sadcp1  16340  pceu  16723  vdwlem12  16869  sgrp2rid2ex  18742  gsumval3eu  19686  lss1d  20439  nrmr0reg  23116  stdbdxmet  23887  xrsxmet  24188  cmetcaulem  24668  bcth3  24711  iundisj2  24929  ulmdvlem3  25777  ulmdv  25778  dchrvmasumlem2  26862  colrot1  27543  lnrot1  27607  lnrot2  27608  wlkson  28646  trlsfval  28685  pthsfval  28711  spthsfval  28712  clwlks  28762  crcts  28778  cycls  28779  3cyclfrgrrn1  29271  frgrwopreg  29309  reuxfrdf  31462  iundisj2f  31554  iundisj2fi  31747  ordtprsuni  32557  pmeasmono  32981  erdszelem9  33850  satfv1fvfmla1  34074  opnrebl2  34839  wl-ifpimpr  35983  wl-df-3xor  35985  wl-ax11-lem9  36091  ax12fromc15  37413  axc16g-o  37442  ax12indalem  37453  ax12inda2ALT  37454  dihopelvalcpre  39757  lpolconN  39996  dvrelog2b  40569  aks6d1c2p2  40595  sticksstones11  40610  fsuppind  40808  zindbi  41313  cnvtrucl0  41984  ismnushort  42669  e2ebind  42933  uunT1  43150  ovnval2  44872  ovnval2b  44879  hoiqssbl  44952  6gbe  46049  8gbe  46051
  Copyright terms: Public domain W3C validator