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  884  dn1  959  2sb6rf  2175  reu8  3292  unass  3654  ssin  3713  difab  3760  csbab  3848  iunss  4359  poirr  4804  cnvuni  5180  dfco2  5497  resin  5828  dffv2  5931  dff1o6  6160  sbthcl  7629  fiint  7786  dfsup2OLD  7892  rankf  8201  dfac3  8491  dfac5lem3  8495  elznn0  10868  elnn1uz2  11147  lsmspsn  17506  usg2spot2nb  24728  h2hlm  25559  cmbr2i  26176  pjss2i  26260  iuninc  27087  dffr5  28745  brsset  29102  brtxpsd  29107  ellines  29365  itg2addnclem3  29632  dvasin  29667  cvlsupr3  34016  dihglb2  36014
  Copyright terms: Public domain W3C validator