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

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

Proof of Theorem 3bitrri
StepHypRef Expression
1 3bitri.3 . 2
2 3bitri.1 . . 3
3 3bitri.2 . . 3
42, 3bitr2i 250 . 2
51, 4bitr3i 251 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  nbbn  358  pm5.17  888  dn1  966  2sb6rf  2196  reu8  3295  unass  3660  ssin  3719  difab  3766  csbab  3855  iunss  4371  poirr  4816  cnvuni  5194  dfco2  5511  resin  5842  dffv2  5946  dff1o6  6181  sbthcl  7659  fiint  7817  dfsup2OLD  7923  rankf  8233  dfac3  8523  dfac5lem3  8527  elznn0  10904  elnn1uz2  11187  lsmspsn  17730  usg2spot2nb  25065  h2hlm  25897  cmbr2i  26514  pjss2i  26598  iuninc  27428  dffr5  29182  brsset  29539  brtxpsd  29544  ellines  29802  itg2addnclem3  30068  dvasin  30103  cvlsupr3  35069  dihglb2  37069  bj-ifidg  37707
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