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

Theorem 3bitr2ri 277
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 255 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitr2i 253 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  xorass  1404  ssrab  3545  copsex2gb  4965  relop  5005  dmopab3  5067  issref  5233  fununi  5667  dffv2  5954  dfsup2  7964  kmlem3  8580  recmulnq  9388  ovoliunlem1  22333  shne0i  26936  ssiun3  28012  cnvoprab  28151  ind1a  28681  bnj1304  29419  bnj1253  29614  dfrecs2  30502  icorempt2  31488  dalem20  32967  rp-isfinite6  35862
  Copyright terms: Public domain W3C validator