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

Theorem 3bitr2ri 266
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 244 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitr2i 242 1  |-  ( th  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  sbnf2  2143  ssrab  3366  relop  4965  dmopab3  5024  issref  5189  fununi  5459  dffv2  5737  copsex2gb  6348  dfsup2  7384  kmlem3  7967  recmulnq  8776  ovoliunlem1  19267  shne0i  22800  ssiun3  23855  ind1a  24216  onfrALTlem5  27973  bnj1304  28531  bnj1253  28726  sbnf2NEW7  28943  dalem20  29809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator