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

Theorem 3bitr2ri 282
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 260 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitr2i 258 1  |-  ( th  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
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 190
This theorem is referenced by:  xorass  1434  ssrab  3493  copsex2gb  4950  relop  4990  dmopab3  5053  issref  5219  fununi  5659  dffv2  5953  dfsup2  7976  kmlem3  8600  recmulnq  9407  ovoliunlem1  22533  shne0i  27182  ssiun3  28251  cnvoprab  28383  ind1a  28916  bnj1304  29703  bnj1253  29898  dfrecs2  30788  icorempt2  31824  dalem20  33329  rp-isfinite6  36234  rababg  36250
  Copyright terms: Public domain W3C validator