MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitrri Structured version   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  3122  unass  3496  ssin  3555  difab  3602  iunss  4124  poirr  4506  cnvuni  5049  dfco2  5361  resin  5689  dffv2  5788  dff1o6  6005  sbthcl  7221  fiint  7375  dfsup2OLD  7440  rankf  7710  dfac3  7992  dfac5lem3  7996  elznn0  10286  elnn1uz2  10542  lsmspsn  16146  h2hlm  22473  cmbr2i  23088  pjss2i  23172  iuninc  24001  dffr5  25366  brsset  25699  brtxpsd  25704  ellines  26051  itg2addnclem3  26221  dvreasin  26243  usg2spot2nb  28355  cvlsupr3  30043  dihglb2  32041
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