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

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

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 3bitr2i.2 . . 3  |-  ( ch  <->  ps )
31, 2bitr4i 245 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 242 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  con2bi  320  an13  776  xorneg1  1321  2eu5  2367  exists1  2372  euxfr  3122  euind  3123  rmo4  3129  2reu5lem3  3143  rmo3  3250  difin  3580  difin0ss  3696  uniuni  4719  reusv2lem4  4730  reusv6OLD  4737  reusv7OLD  4738  rabxp  4917  eliunxp  5015  imadisj  5226  intirr  5255  resco  5377  funcnv3  5515  fncnv  5518  fun11  5519  fununi  5520  f1mpt  6010  mpt2mptx  6167  frxp  6459  oeeu  6849  ixp0x  7093  mapsnen  7187  xpcomco  7201  1sdom  7314  dffi3  7439  cardval3  7844  kmlem4  8038  kmlem12  8046  kmlem14  8048  kmlem15  8049  kmlem16  8050  fpwwe2  8523  axgroth4  8712  ltexprlem4  8921  bitsmod  12953  pythagtrip  13213  pgpfac1  15643  pgpfac  15647  isassa  16380  istps3OLD  16992  basdif0  17023  ntreq0  17146  tgcmp  17469  tx1cn  17646  rnelfmlem  17989  phtpcer  19025  caucfil  19241  minveclem1  19330  ovoliunlem1  19403  mdegleb  19992  3v3e3cycl2  21656  adjbd1o  23593  nmo  23978  rmo3f  23987  rmo4fOLD  23988  mptfnf  24078  1stmbfm  24615  cvmlift2lem12  25006  axacprim  25161  andnand1  26153  itg2addnc  26272  fgraphopab  27519  ndmaovcom  28058  usgra2pth0  28349  iswwlk  28364  onfrALTlem5  28701  bnj976  29221  bnj1143  29234  bnj1533  29296  bnj864  29366  bnj983  29395  bnj1174  29445  bnj1175  29446  bnj1280  29462  isopos  30051  dihglblem6  32211  dihglb2  32213
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 179
  Copyright terms: Public domain W3C validator