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

Theorem 3bitrri 264
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 242 . 2  |-  ( ch  <->  ph )
51, 4bitr3i 243 1  |-  ( th  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  nbbn  348  pm5.17  859  dn1  933  reu8  3074  unass  3448  ssin  3507  difab  3554  iunss  4074  poirr  4456  cnvuni  4998  dfco2  5310  resin  5638  dffv2  5736  dff1o6  5953  sbthcl  7166  fiint  7320  dfsup2OLD  7384  rankf  7654  dfac3  7936  dfac5lem3  7940  elznn0  10229  elnn1uz2  10485  lsmspsn  16084  h2hlm  22332  cmbr2i  22947  pjss2i  23031  iuninc  23856  dffr5  25135  brsset  25454  brtxpsd  25459  ellines  25801  itg2addnc  25960  dvreasin  25981  cvlsupr3  29460  dihglb2  31458
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 178
  Copyright terms: Public domain W3C validator