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

Theorem biid 228
Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
biid

Proof of Theorem biid
StepHypRef Expression
1 id 20 . 2
21, 1impbii 181 1
Colors of variables: wff set class
Syntax hints:  <->wb 177
This theorem is referenced by:  biidd  229  pm5.19  350  3anbi1i  1144  3anbi2i  1145  3anbi3i  1146  trujust  1327  tru  1330  trubitru  1359  falbifal  1362  hadcoma  1397  hadcomb  1398  hadnot  1402  cadcomb  1405  eqid  2435  abid2  2552  abid2f  2596  ceqsexg  3059  wecmpep  4566  ordon  4755  sorpss  6519  tz7.49c  6695  dford2  7567  infxpen  7888  isacn  7917  dfac5  8001  dfackm  8038  pwfseq  8531  axgroth5  8691  axgroth6  8695  supmul  9968  fsum2d  12547  rpnnen2  12817  isstruct  13471  oppccatid  13937  subccatid  14035  fuccatid  14158  setccatid  14231  catccatid  14249  xpccatid  14277  spwpr4  14655  opprsubg  15733  abvtriv  15921  lmodvscl  15959  opsrtos  16538  iscnp2  17295  cbvditg  19733  ditgsplit  19740  lgsquad2  21136  nb3grapr  21454  eqid1  21753  grpoidinv  21788  stri  23752  hstri  23760  stcltrthi  23773  nmo  23965  elxrge02  24170  cvmliftlem11  24974  cbvprod  25233  fprod2d  25297  socnv  25380  dfon2  25411  sltsolem1  25615  brpprod3b  25724  brapply  25775  brrestrict  25786  dfrdg4  25787  cgr3permute3  25973  cgr3permute1  25974  cgr3permute2  25975  cgr3permute4  25976  cgr3permute5  25977  colinearxfr  26001  brsegle  26034  rngunsnply  27346  symgsssg  27376  symgfisg  27377  iotaequ  27597  frgra3v  28329  2uasban  28586  e2ebindVD  28961  e2ebindALT  28978  iunconALT  28985  bnj1383  29140  bnj1386  29142  bnj153  29188  bnj543  29201  bnj544  29202  bnj546  29204  bnj605  29215  bnj579  29222  bnj600  29227  bnj601  29228  bnj852  29229  bnj893  29236  bnj906  29238  bnj917  29242  bnj938  29245  bnj944  29246  bnj998  29264  bnj1006  29267  bnj1029  29274  bnj1034  29276  bnj1124  29294  bnj1128  29296  bnj1127  29297  bnj1125  29298  bnj1147  29300  bnj1190  29314  bnj69  29316  bnj1204  29318  bnj1311  29330  bnj1318  29331  bnj1384  29338  bnj1408  29342  bnj1414  29343  bnj1415  29344  bnj1421  29348  bnj1423  29357  bnj1489  29362  bnj1493  29365  bnj60  29368  bnj1500  29374  bnj1522  29378  dalemeea  30397  dalem4  30399  dalem6  30402  dalem7  30403  dalem11  30408  dalem12  30409  dalem29  30435  dalem30  30436  dalem31N  30437  dalem32  30438  dalem33  30439  dalem34  30440  dalem35  30441  dalem36  30442  dalem37  30443  dalem40  30446  dalem46  30452  dalem47  30453  dalem49  30455  dalem50  30456  dalem52  30458  dalem53  30459  dalem54  30460  dalem56  30462  dalem58  30464  dalem59  30465  dalem62  30468  paddval  30532  4atexlemex4  30807  4atexlemex6  30808  cdleme31sdnN  31121  cdlemefr44  31159  cdleme48fv  31233  cdlemeg49lebilem  31273  cdleme50eq  31275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator