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  2974  unass  3345  ssin  3404  difab  3450  iunss  3959  poirr  4341  cnvuni  4882  dfco2  5188  resin  5511  dffv2  5608  dff1o6  5807  sbthcl  6999  fiint  7149  dfsup2OLD  7212  rankf  7482  dfac3  7764  dfac5lem3  7768  elznn0  10054  elnn1uz2  10310  lsmspsn  15853  h2hlm  21576  cmbr2i  22191  pjss2i  22275  dffr5  24181  brsset  24500  brtxpsd  24505  ellines  24847  itg2addnc  25005  dvreasin  25026  cvlsupr3  30156  dihglb2  32154
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