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  888  dn1  966  2sb6rf  2182  reu8  3281  unass  3646  ssin  3705  difab  3752  csbab  3841  iunss  4356  poirr  4801  cnvuni  5179  dfco2  5496  resin  5827  dffv2  5931  dff1o6  6166  sbthcl  7641  fiint  7799  dfsup2OLD  7905  rankf  8215  dfac3  8505  dfac5lem3  8509  elznn0  10886  elnn1uz2  11168  lsmspsn  17708  usg2spot2nb  25041  h2hlm  25873  cmbr2i  26490  pjss2i  26574  iuninc  27404  dffr5  29157  brsset  29514  brtxpsd  29519  ellines  29777  itg2addnclem3  30043  dvasin  30078  cvlsupr3  34809  dihglb2  36809
  Copyright terms: Public domain W3C validator