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

Theorem 3bitr3ri 269
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 244 . 2  |-  ( ps  <->  ch )
51, 4bitr3i 244 1  |-  ( th  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  bigolden  903  2eu8  2370  2ralor  2879  sbcco  3185  dfiin2g  4126  zfpair  4403  dffun6f  5470  fsplit  6453  tfrlem2  6639  axdc3lem4  8335  gtiso  24090  qqhre  24388  dfpo2  25380  dfdm5  25402  dfrn5  25403  nofulllem5  25663  symdifass  25674  brimg  25784  elnev  27617  2reu8  27948  cdlemefrs29bpre0  31255  cdlemftr3  31424
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 179
  Copyright terms: Public domain W3C validator