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

Theorem 3bitrri 263
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 241 . 2  |-  ( ch  <->  ph )
51, 4bitr3i 242 1  |-  ( th  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  nbbn  347  pm5.17  858  dn1  932  reu8  2961  unass  3332  ssin  3391  difab  3437  iunss  3943  poirr  4325  cnvuni  4866  dfco2  5172  resin  5495  dffv2  5592  dff1o6  5791  sbthcl  6983  fiint  7133  dfsup2OLD  7196  rankf  7466  dfac3  7748  dfac5lem3  7752  elznn0  10038  elnn1uz2  10294  lsmspsn  15837  h2hlm  21560  cmbr2i  22175  pjss2i  22259  dffr5  24110  brsset  24429  brtxpsd  24434  ellines  24775  dvreasin  24923  cvlsupr3  29534  dihglb2  31532
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator