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  1590  cbval2  1957  cbvex2  1958  sbco2d  2040  equsb3  2054  elsb3  2055  elsb4  2056  sbcom2  2066  dfsb7  2071  sb7f  2072  eq2tri  2355  eqsb3  2397  clelsb3  2398  r19.35  2700  ralcom4  2819  rexcom4  2820  ceqsralt  2824  gencbvex  2843  gencbval  2845  ceqsrexbv  2915  euind  2965  reuind  2981  sbccomlem  3074  sbccom  3075  difcom  3551  uniintsn  3915  disjxun  4037  exss  4252  reusv2lem4  4554  elxp2  4723  eqbrriv  4798  dm0rn0  4911  dfres2  5018  qfto  5080  rninxp  5133  fununi  5332  dffv2  5608  fndmin  5648  dfoprab2  5911  dfer2  6677  eceqoveq  6779  euen1  6947  xpsnen  6962  xpassen  6972  marypha2lem3  7206  rankuni  7551  card1  7617  alephislim  7726  dfacacn  7783  kmlem4  7795  ac6num  8122  zorn2lem4  8142  fpwwe2lem8  8275  fpwwe2lem12  8279  mappsrpr  8746  sqeqori  11231  vdwmc2  13042  txflf  17717  caucfil  18725  ovolgelb  18855  nmoubi  21366  hvsubaddi  21661  hlimeui  21836  omlsilem  21997  pjoml3i  22181  hodsi  22371  nmopub  22504  nmfnleub  22521  nmopcoadj0i  22699  pjin3i  22790  ralcom4f  23149  rexcom4f  23150  clelsb3f  23158  br1steq  24201  br2ndeq  24202  brimg  24547  brfullfun  24558  axcontlem5  24668  eeeeanv  25047  negcmpprcal2  25049  filnetlem4  26433  moxfr  26855  coeq0  26934  pm11.6  27694  nbusgra  28277  cbvexsv  28611  bnj62  29062  bnj610  29092  bnj1143  29138  bnj1533  29200  bnj543  29241  bnj545  29243  bnj594  29260  sbco2dwAUX7  29560  equsb3NEW7  29574  elsb3NEW7  29575  elsb4NEW7  29576  cbval2OLD7  29684  cbvex2OLD7  29685  sbco2dOLD7  29707  sbcom2OLD7  29715  dfsb7OLD7  29719  sb7fOLD7  29720  isltrn2N  30931
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