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

Theorem 3bitr2i 273
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1
3bitr2i.2
3bitr2i.3
Assertion
Ref Expression
3bitr2i

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3
2 3bitr2i.2 . . 3
31, 2bitr4i 252 . 2
4 3bitr2i.3 . 2
53, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  con2bi  328  an13  799  xorneg1  1373  2eu4  2380  2eu5  2382  exists1  2388  euxfr  3285  euind  3286  rmo4  3292  2reu5lem3  3307  rmo3  3429  difin  3734  difin0ss  3894  reusv2lem4  4656  reusv6OLD  4663  reusv7OLD  4664  rabxp  5041  eliunxp  5145  imadisj  5361  intirr  5390  resco  5516  funcnv3  5654  fncnv  5657  fun11  5658  fununi  5659  f1mpt  6169  mpt2mptx  6393  uniuni  6609  frxp  6910  oeeu  7271  ixp0x  7517  mapsnen  7613  xpcomco  7627  1sdom  7742  dffi3  7911  wemapsolem  7996  cardval3  8354  kmlem4  8554  kmlem12  8562  kmlem14  8564  kmlem15  8565  kmlem16  8566  fpwwe2  9042  axgroth4  9231  ltexprlem4  9438  bitsmod  14086  pythagtrip  14358  pgpfac1  17131  pgpfac  17135  isassa  17964  istps3OLD  19423  basdif0  19454  ntreq0  19578  tgcmp  19901  tx1cn  20110  rnelfmlem  20453  phtpcer  21495  caucfil  21722  minveclem1  21839  ovoliunlem1  21913  mdegleb  22464  istrkg2ld  23858  3v3e3cycl2  24664  iswwlk  24683  adjbd1o  27004  nmo  27384  rmo3f  27394  rmo4fOLD  27395  mptfnf  27499  mpt2mptxf  27518  1stmbfm  28231  cvmlift2lem12  28759  axacprim  29079  andnand1  29864  itg2addnc  30069  asindmre  30102  fgraphopab  31170  ndmaovcom  32290  usgra2pth0  32355  eliunxp2  32923  mpt2mptx2  32924  alimp-no-surprise  33196  alsi-no-surprise  33211  onfrALTlem5  33314  bnj976  33836  bnj1143  33849  bnj1533  33910  bnj864  33980  bnj983  34009  bnj1174  34059  bnj1175  34060  bnj1280  34076  bj-denotes  34434  bj-snglc  34527  isopos  34905  dihglblem6  37067  dihglb2  37069  bj-ifid2g  37709  rp-fakeanorass  37737  elintima  37765
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