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

Theorem 3bitr3ri 267
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1  |-  ( ph  <->  ps )
3bitr3i.2  |-  ( ph  <->  ch )
3bitr3i.3  |-  ( ps  <->  th )
Assertion
Ref Expression
3bitr3ri  |-  ( th  <->  ch )

Proof of Theorem 3bitr3ri
StepHypRef Expression
1 3bitr3i.3 . 2  |-  ( ps  <->  th )
2 3bitr3i.1 . . 3  |-  ( ph  <->  ps )
3 3bitr3i.2 . . 3  |-  ( ph  <->  ch )
42, 3bitr3i 242 . 2  |-  ( ps  <->  ch )
51, 4bitr3i 242 1  |-  ( th  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bigolden  901  2eu8  2230  2ralor  2709  sbcco  3013  dfiin2g  3936  zfpair  4212  pwundifOLD  4301  dffun6f  5269  fsplit  6223  tfrlem2  6392  axdc3lem4  8079  ballotlem2  23047  gtiso  23241  dfpo2  24112  dfdm5  24132  dfrn5  24133  nofulllem5  24360  symdifass  24371  dffun10  24453  elfuns  24454  elnev  27638  2reu8  27970  a12study8  29119  cdlemefrs29bpre0  30585  cdlemftr3  30754
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