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

Theorem 3bitr3ri 268
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 243 . 2  |-  ( ps  <->  ch )
51, 4bitr3i 243 1  |-  ( th  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bigolden  902  2eu8  2341  2ralor  2837  sbcco  3143  dfiin2g  4084  zfpair  4361  dffun6f  5427  fsplit  6410  tfrlem2  6596  axdc3lem4  8289  gtiso  24041  qqhre  24339  dfpo2  25326  dfdm5  25346  dfrn5  25347  nofulllem5  25574  symdifass  25585  dffun10  25667  elfuns  25668  elnev  27506  2reu8  27837  cdlemefrs29bpre0  30878  cdlemftr3  31047
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