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

Theorem 3bitrri 275
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 253 . 2  |-  ( ch  <->  ph )
51, 4bitr3i 254 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  nbbn  359  pm5.17  896  dn1  974  2sb6rf  2247  reu8  3267  unass  3623  ssin  3684  difab  3742  csbab  3825  iunss  4337  poirr  4782  cnvuni  5037  dfco2  5350  resin  5849  dffv2  5951  dff1o6  6186  sbthcl  7697  fiint  7851  rankf  8267  dfac3  8553  dfac5lem3  8557  elznn0  10953  elnn1uz2  11236  lsmspsn  18295  usg2spot2nb  25779  h2hlm  26619  cmbr2i  27235  pjss2i  27319  iuninc  28166  dffr5  30388  brsset  30649  brtxpsd  30654  ellines  30912  itg2addnclem3  31909  dvasin  31942  cvlsupr3  32829  dihglb2  34829  ifpidg  36055  ss2iundf  36111  dffrege76  36393  dffrege99  36416  disjinfi  37318
  Copyright terms: Public domain W3C validator