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

Theorem 3bitr2ri 274
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1  |-  ( ph  <->  ps )
3bitr2i.2  |-  ( ch  <->  ps )
3bitr2i.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitr2ri  |-  ( th  <->  ph )

Proof of Theorem 3bitr2ri
StepHypRef Expression
1 3bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 3bitr2i.2 . . 3  |-  ( ch  <->  ps )
31, 2bitr4i 252 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitr2i 250 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  sbnf2OLD  2153  ssrab  3533  copsex2gb  5053  relop  5093  dmopab3  5155  issref  5314  fununi  5587  dffv2  5868  dfsup2  7798  kmlem3  8427  recmulnq  9239  ovoliunlem1  21112  shne0i  24998  ssiun3  26055  cnvoprab  26169  ind1a  26617  bnj1304  32126  bnj1253  32321  dalem20  33656
  Copyright terms: Public domain W3C validator