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

Theorem 3bitr3i 275
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1  |-  ( ph  <->  ps )
3bitr3i.2  |-  ( ph  <->  ch )
3bitr3i.3  |-  ( ps  <->  th )
Assertion
Ref Expression
3bitr3i  |-  ( ch  <->  th )

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3  |-  ( ph  <->  ch )
2 3bitr3i.1 . . 3  |-  ( ph  <->  ps )
31, 2bitr3i 251 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 249 1  |-  ( ch  <->  th )
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:  an12  795  cadanOLD  1444  19.35OLD  1665  cbval2  2000  cbvex2OLD  2002  sbco2d  2136  sbcom  2139  equsb3  2159  equsb3ALT  2160  elsb3  2161  elsb4  2162  sbcom2OLD  2174  sb7f  2185  sbco4lem  2200  eq2tri  2535  eqsb3  2587  clelsb3  2588  r19.35  3008  ralcom4  3132  rexcom4  3133  ceqsralt  3137  gencbvex  3157  gencbval  3159  ceqsrexbv  3238  euind  3290  reuind  3307  sbccomlem  3410  sbccom  3411  csbcom  3837  difcom  3911  uniintsn  4319  disjxun  4445  reusv2lem4  4651  exss  4710  elxp2  5017  eqbrriv  5096  dm0rn0  5217  dfres2  5324  qfto  5386  rninxp  5444  coeq0  5514  fununi  5652  dffv2  5938  fndmin  5986  fnprb  6117  dfoprab2  6325  dfer2  7309  eceqoveq  7413  euen1  7582  xpsnen  7598  xpassen  7608  marypha2lem3  7893  rankuni  8277  card1  8345  alephislim  8460  dfacacn  8517  kmlem4  8529  ac6num  8855  zorn2lem4  8875  fpwwe2lem8  9011  fpwwe2lem12  9015  mappsrpr  9481  sqeqori  12244  vdwmc2  14352  txflf  20242  metustidOLD  20797  metustid  20798  caucfil  21457  ovolgelb  21626  axcontlem5  23947  nmoubi  25363  hvsubaddi  25659  hlimeui  25834  omlsilem  25996  pjoml3i  26180  hodsi  26370  nmopub  26503  nmfnleub  26520  nmopcoadj0i  26698  pjin3i  26789  or3dir  27044  ralcom4f  27051  rexcom4f  27052  clelsb3f  27055  ordtconlem1  27542  br1steq  28781  br2ndeq  28782  elima4  28786  brfullfun  29175  filnetlem4  29802  moxfr  30228  hashnzfzclim  30827  pm11.6  30876  sbc3or  32381  cbvexsv  32399  bnj62  32853  bnj610  32883  bnj1143  32928  bnj1533  32989  bnj543  33030  bnj545  33032  bnj594  33049  bj-cbval2v  33384  bj-clelsb3  33505  isltrn2N  34916  trclubg  36795
  Copyright terms: Public domain W3C validator