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

Theorem 3bitr3i 266
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 242 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 240 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  an12  772  cadan  1382  19.35  1587  cbval2  1944  cbvex2  1945  sbco2d  2027  equsb3  2041  elsb3  2042  elsb4  2043  sbcom2  2053  dfsb7  2058  sb7f  2059  eq2tri  2342  eqsb3  2384  clelsb3  2385  r19.35  2687  ralcom4  2806  rexcom4  2807  ceqsralt  2811  gencbvex  2830  gencbval  2832  ceqsrexbv  2902  euind  2952  reuind  2968  sbccomlem  3061  sbccom  3062  difcom  3538  uniintsn  3899  disjxun  4021  exss  4236  reusv2lem4  4538  elxp2  4707  eqbrriv  4782  dm0rn0  4895  dfres2  5002  qfto  5064  rninxp  5117  fununi  5316  dffv2  5592  fndmin  5632  dfoprab2  5895  dfer2  6661  eceqoveq  6763  euen1  6931  xpsnen  6946  xpassen  6956  marypha2lem3  7190  rankuni  7535  card1  7601  alephislim  7710  dfacacn  7767  kmlem4  7779  ac6num  8106  zorn2lem4  8126  fpwwe2lem8  8259  fpwwe2lem12  8263  mappsrpr  8730  sqeqori  11215  vdwmc2  13026  txflf  17701  caucfil  18709  ovolgelb  18839  nmoubi  21350  hvsubaddi  21645  hlimeui  21820  omlsilem  21981  pjoml3i  22165  hodsi  22355  nmopub  22488  nmfnleub  22505  nmopcoadj0i  22683  pjin3i  22774  ralcom4f  23133  rexcom4f  23134  clelsb3f  23142  br1steq  24130  br2ndeq  24131  brimg  24476  brfullfun  24486  axcontlem5  24596  eeeeanv  24944  negcmpprcal2  24946  filnetlem4  26330  moxfr  26752  coeq0  26831  pm11.6  27591  nbusgra  28143  cbvexsv  28312  bnj62  28746  bnj610  28776  bnj1143  28822  bnj1533  28884  bnj543  28925  bnj545  28927  bnj594  28944  isltrn2N  30309
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 177
  Copyright terms: Public domain W3C validator