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  2243  2ralor  2722  sbcco  3026  dfiin2g  3952  zfpair  4228  pwundifOLD  4317  dffun6f  5285  fsplit  6239  tfrlem2  6408  axdc3lem4  8095  ballotlem2  23063  gtiso  23256  dfpo2  24183  dfdm5  24203  dfrn5  24204  nofulllem5  24431  symdifass  24442  dffun10  24524  elfuns  24525  elnev  27741  2reu8  28073  a12study8  29741  cdlemefrs29bpre0  31207  cdlemftr3  31376
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