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

Theorem 3bitr2ri 278
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 256 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitr2i 254 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188
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 189
This theorem is referenced by:  xorass  1408  ssrab  3506  copsex2gb  4944  relop  4984  dmopab3  5046  issref  5212  fununi  5647  dffv2  5936  dfsup2  7955  kmlem3  8579  recmulnq  9386  ovoliunlem1  22448  shne0i  27094  ssiun3  28166  cnvoprab  28301  ind1a  28835  bnj1304  29624  bnj1253  29819  dfrecs2  30710  icorempt2  31747  dalem20  33252  rp-isfinite6  36157  rababg  36173
  Copyright terms: Public domain W3C validator