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

Theorem 3bitr3i 278
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 254 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 252 1  |-  ( ch  <->  th )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  an12  804  xorass  1404  19.35OLD  1735  cbval2  2083  sbco2d  2211  sbcom  2213  equsb3  2228  equsb3ALT  2229  elsb3  2230  elsb4  2231  sb7f  2249  sbco4lem  2261  eq2tri  2497  eqsb3  2549  clelsb3  2550  r19.35  2982  ralcom4  3106  rexcom4  3107  ceqsralt  3111  gencbvex  3131  gencbval  3133  ceqsrexbv  3212  euind  3264  reuind  3281  sbccomlem  3376  sbccom  3377  csbcom  3817  difcom  3886  uniintsn  4296  disjxun  4424  reusv2lem4  4629  exss  4685  elxp2  4872  eqbrriv  4950  dm0rn0  5071  dfres2  5177  qfto  5241  rninxp  5296  coeq0  5364  fununi  5667  dffv2  5954  fndmin  6004  fnprb  6138  dfoprab2  6351  dfer2  7372  eceqoveq  7476  euen1  7646  xpsnen  7662  xpassen  7672  marypha2lem3  7957  rankuni  8333  card1  8401  alephislim  8512  dfacacn  8569  kmlem4  8581  ac6num  8907  zorn2lem4  8927  fpwwe2lem8  9061  fpwwe2lem12  9065  mappsrpr  9531  sqeqori  12383  trclublem  13038  fprodle  14028  vdwmc2  14892  txflf  20952  metustid  21500  caucfil  22146  ovolgelb  22311  dfcgra2  24726  axcontlem5  24844  nmoubi  26258  hvsubaddi  26554  hlimeui  26728  omlsilem  26890  pjoml3i  27074  hodsi  27263  nmopub  27396  nmfnleub  27413  nmopcoadj0i  27591  pjin3i  27682  or3dir  27937  ralcom4f  27945  rexcom4f  27946  clelsb3f  27951  uniinn0  28002  ordtconlem1  28569  bnj62  29314  bnj610  29345  bnj1143  29390  bnj1533  29451  bnj543  29492  bnj545  29494  bnj594  29511  br1steq  30201  br2ndeq  30202  elima4  30208  brsuccf  30493  brfullfun  30500  filnetlem4  30822  bj-cbval2v  31082  bj-clelsb3  31208  icorempt2  31488  poimirlem13  31657  poimirlem14  31658  poimirlem21  31665  poimirlem22  31666  poimir  31677  sbccom2lem  32068  isltrn2N  33394  moxfr  35243  ifporcor  35804  ifpancor  35806  ifpbicor  35818  ifpnorcor  35823  ifpnancor  35824  ifpororb  35848  relexp0eq  35932  hashnzfzclim  36308  pm11.6  36379  sbc3or  36526  cbvexsv  36550  copisnmnd  38567
  Copyright terms: Public domain W3C validator