MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitrri Structured version   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  |-  ( 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 250 . 2  |-  ( ch  <->  ph )
51, 4bitr3i 251 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
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
This theorem is referenced by:  nbbn  358  pm5.17  883  dn1  957  2sb6rf  2160  reu8  3153  unass  3511  ssin  3570  difab  3617  csbab  3705  iunss  4209  poirr  4650  cnvuni  5024  dfco2  5335  resin  5660  dffv2  5762  dff1o6  5980  sbthcl  7431  fiint  7586  dfsup2OLD  7691  rankf  7999  dfac3  8289  dfac5lem3  8293  elznn0  10659  elnn1uz2  10929  lsmspsn  17163  h2hlm  24380  cmbr2i  24997  pjss2i  25081  iuninc  25909  dffr5  27561  brsset  27918  brtxpsd  27923  ellines  28181  itg2addnclem3  28442  dvasin  28477  usg2spot2nb  30655  cvlsupr3  32986  dihglb2  34984
  Copyright terms: Public domain W3C validator