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

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

Proof of Theorem biidd
StepHypRef Expression
1 biid 236 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3anbi12d  1300  3anbi13d  1301  3anbi23d  1302  3anbi1d  1303  3anbi2d  1304  3anbi3d  1305  had1  1470  nfald2  2073  exdistrf  2075  axc16gALT  2106  sb6x  2125  ax12  2234  ax16g-o  2264  ax12indalem  2275  ax12inda2ALT  2276  ralxpxfr2d  3224  rr19.3v  3241  rr19.28v  3242  moeq3  3276  euxfr2  3284  dfif3  3955  sseliALT  4583  reuxfr2d  4675  copsexg  4737  copsexgOLD  4738  soeq1  4824  ordtri3or  4915  soinxp  5069  ov6g  6440  ovg  6441  sorpssi  6586  dfxp3  6860  aceq1  8519  aceq2  8521  axpowndlem4  8998  axpownd  8999  ltsopr  9431  creur  10555  creui  10556  o1fsum  13627  sadfval  14102  sadcp1  14105  pceu  14370  vdwlem12  14510  coafval  15391  sgrp2rid2ex  16045  gsumval3eu  16907  dprdval  17034  dprdvalOLD  17036  lss1d  17609  nrmr0reg  20250  stdbdxmet  21018  xrsxmet  21314  cmetcaulem  21727  bcth3  21770  iundisj2  21959  ulmdvlem3  22797  ulmdv  22798  dchrvmasumlem2  23683  colrot1  23946  lnrot1  24003  lnrot2  24004  eengv  24282  isausgra  24354  usgraeq12d  24362  usgra0v  24371  usgra1v  24390  2pthoncl  24605  crcts  24622  cycls  24623  3cyclfrgrarn1  25012  frgraregorufr0  25052  reuxfr3d  27388  iundisj2f  27449  iundisj2fi  27602  ordtprsuni  27901  isrnsigaOLD  28112  erdszelem9  28643  mpstval  28895  wl-ax11-lem9  30033  opnrebl2  30139  zindbi  30882  e2ebind  33336  uunT1  33577  trsbcVD  33677  pclfvalN  35613  dihopelvalcpre  36975  lpolconN  37214
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 185
  Copyright terms: Public domain W3C validator