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:  ssrab  3574  copsex2gb  5122  relop  5163  dmopab3  5225  issref  5390  fununi  5660  dffv2  5946  dfsup2  7920  kmlem3  8549  recmulnq  9359  ovoliunlem1  22038  shne0i  26492  ssiun3  27562  cnvoprab  27696  ind1a  28187  bnj1304  33979  bnj1253  34174  dalem20  35518  rp-isfinite6  37845
  Copyright terms: Public domain W3C validator