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

Theorem 3bitr2i 265
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
3bitr2i  |-  ( ph  <->  th )

Proof of Theorem 3bitr2i
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, 4bitri 241 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  con2bi  319  an13  775  xorneg1  1317  2eu5  2323  exists1  2328  euxfr  3064  euind  3065  rmo4  3071  2reu5lem3  3085  rmo3  3192  difin  3522  difin0ss  3638  uniuni  4657  reusv2lem4  4668  reusv6OLD  4675  reusv7OLD  4676  rabxp  4855  eliunxp  4953  imadisj  5164  intirr  5193  resco  5315  funcnv3  5453  fncnv  5456  fun11  5457  fununi  5458  f1mpt  5947  mpt2mptx  6104  frxp  6393  oeeu  6783  ixp0x  7027  mapsnen  7121  xpcomco  7135  1sdom  7248  dffi3  7372  cardval3  7773  kmlem4  7967  kmlem12  7975  kmlem14  7977  kmlem15  7978  kmlem16  7979  fpwwe2  8452  axgroth4  8641  ltexprlem4  8850  bitsmod  12876  pythagtrip  13136  pgpfac1  15566  pgpfac  15570  isassa  16303  istps3OLD  16911  basdif0  16942  ntreq0  17065  tgcmp  17387  tx1cn  17563  rnelfmlem  17906  phtpcer  18892  caucfil  19108  minveclem1  19193  ovoliunlem1  19266  mdegleb  19855  3v3e3cycl2  21500  adjbd1o  23437  nmo  23818  rmo3f  23827  rmo4fOLD  23828  mptfnf  23916  1stmbfm  24405  cvmlift2lem12  24781  axacprim  24936  brimg  25501  andnand1  25863  itg2addnc  25960  fgraphopab  27199  ndmaovcom  27739  onfrALTlem5  27972  bnj976  28487  bnj1143  28500  bnj1533  28562  bnj864  28632  bnj983  28661  bnj1174  28711  bnj1175  28712  bnj1280  28728  isopos  29296  dihglblem6  31456  dihglb2  31458
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