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  cbval2  2086  sbco2d  2215  sbcom  2217  equsb3  2232  equsb3ALT  2233  elsb3  2234  elsb4  2235  sb7f  2253  sbco4lem  2265  eq2tri  2483  eqsb3  2527  clelsb3  2528  r19.35  2908  ralcom4  3036  rexcom4  3037  ceqsralt  3041  gencbvex  3061  gencbval  3063  ceqsrexbv  3141  euind  3193  reuind  3211  sbccomlem  3306  sbccom  3307  csbcom  3749  difcom  3818  uniintsn  4229  disjxun  4357  reusv2lem4  4564  exss  4620  elxp2  4807  eqbrriv  4885  dm0rn0  5006  dfres2  5112  qfto  5176  rninxp  5231  coeq0  5299  fununi  5603  dffv2  5891  fndmin  5941  fnprb  6075  dfoprab2  6288  dfer2  7312  eceqoveq  7416  euen1  7586  xpsnen  7602  xpassen  7612  marypha2lem3  7897  rankuni  8279  card1  8347  alephislim  8458  dfacacn  8515  kmlem4  8527  ac6num  8853  zorn2lem4  8873  fpwwe2lem8  9006  fpwwe2lem12  9010  mappsrpr  9476  sqeqori  12329  trclublem  12996  fprodle  13986  vdwmc2  14865  txflf  20956  metustid  21504  caucfil  22188  ovolgelb  22368  dfcgra2  24806  axcontlem5  24933  nmoubi  26348  hvsubaddi  26654  hlimeui  26828  omlsilem  26990  pjoml3i  27174  hodsi  27363  nmopub  27496  nmfnleub  27513  nmopcoadj0i  27691  pjin3i  27782  or3dir  28037  ralcom4f  28045  rexcom4f  28046  clelsb3f  28051  uniinn0  28102  ordtconlem1  28675  bnj62  29471  bnj610  29502  bnj1143  29547  bnj1533  29608  bnj543  29649  bnj545  29651  bnj594  29668  br1steq  30358  br2ndeq  30359  elima4  30365  brsuccf  30650  brfullfun  30657  filnetlem4  30979  bj-cbval2v  31239  bj-clelsb3  31364  icorempt2  31655  poimirlem13  31854  poimirlem14  31855  poimirlem21  31862  poimirlem22  31863  poimir  31874  sbccom2lem  32265  isltrn2N  33591  moxfr  35440  ifporcor  36012  ifpancor  36014  ifpbicor  36026  ifpnorcor  36031  ifpnancor  36032  ifpororb  36056  relexp0eq  36200  hashnzfzclim  36578  pm11.6  36649  sbc3or  36796  cbvexsv  36820  copisnmnd  39394
  Copyright terms: Public domain W3C validator