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

Theorem 3bitrri 276
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitri.1  |-  ( ph  <->  ps )
3bitri.2  |-  ( ps  <->  ch )
3bitri.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitrri  |-  ( th  <->  ph )

Proof of Theorem 3bitrri
StepHypRef Expression
1 3bitri.3 . 2  |-  ( ch  <->  th )
2 3bitri.1 . . 3  |-  ( ph  <->  ps )
3 3bitri.2 . . 3  |-  ( ps  <->  ch )
42, 3bitr2i 254 . 2  |-  ( ch  <->  ph )
51, 4bitr3i 255 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188
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 189
This theorem is referenced by:  nbbn  360  pm5.17  899  dn1  977  2sb6rf  2281  reu8  3234  unass  3591  ssin  3654  difab  3712  csbab  3797  iunss  4319  poirr  4766  cnvuni  5021  dfco2  5334  resin  5835  dffv2  5938  dff1o6  6174  sbthcl  7694  fiint  7848  rankf  8265  dfac3  8552  dfac5lem3  8556  elznn0  10952  elnn1uz2  11235  lsmspsn  18307  usg2spot2nb  25793  h2hlm  26633  cmbr2i  27249  pjss2i  27333  iuninc  28176  dffr5  30393  brsset  30656  brtxpsd  30661  ellines  30919  itg2addnclem3  31995  dvasin  32028  cvlsupr3  32910  dihglb2  34910  ifpidg  36135  ss2iundf  36251  dffrege76  36535  dffrege99  36558  disjinfi  37468  nbgrel  39410
  Copyright terms: Public domain W3C validator