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  1434  19.35OLD  1655  cbval2  1975  cbvex2OLD  1977  sbco2d  2113  sbcom  2116  equsb3  2137  equsb3ALT  2138  elsb3  2139  elsb4  2140  sbcom2OLD  2152  sb7f  2163  sbco4lem  2178  eq2tri  2497  eqsb3  2539  clelsb3  2540  r19.35  2862  ralcom4  2986  rexcom4  2987  ceqsralt  2991  gencbvex  3011  gencbval  3013  ceqsrexbv  3089  euind  3141  reuind  3157  sbccomlem  3260  sbccom  3261  csbcom  3684  difcom  3758  uniintsn  4160  disjxun  4285  reusv2lem4  4491  exss  4550  elxp2  4853  eqbrriv  4930  dm0rn0  5051  dfres2  5153  qfto  5214  rninxp  5272  fununi  5479  dffv2  5759  fndmin  5805  fnprb  5931  dfoprab2  6128  dfer2  7094  eceqoveq  7197  euen1  7371  xpsnen  7387  xpassen  7397  marypha2lem3  7679  rankuni  8062  card1  8130  alephislim  8245  dfacacn  8302  kmlem4  8314  ac6num  8640  zorn2lem4  8660  fpwwe2lem8  8796  fpwwe2lem12  8800  mappsrpr  9267  sqeqori  11970  vdwmc2  14032  txflf  19554  metustidOLD  20109  metustid  20110  caucfil  20769  ovolgelb  20938  axcontlem5  23165  nmoubi  24123  hvsubaddi  24419  hlimeui  24594  omlsilem  24756  pjoml3i  24940  hodsi  25130  nmopub  25263  nmfnleub  25280  nmopcoadj0i  25458  pjin3i  25549  or3dir  25804  ralcom4f  25811  rexcom4f  25812  clelsb3f  25815  ordtconlem1  26306  br1steq  27536  br2ndeq  27537  elima4  27541  brfullfun  27930  filnetlem4  28555  moxfr  28981  coeq0  29043  pm11.6  29598  sbc3or  31124  cbvexsv  31142  bnj62  31596  bnj610  31626  bnj1143  31671  bnj1533  31732  bnj543  31773  bnj545  31775  bnj594  31792  bj-cbval2v  32095  bj-clelsb3  32208  isltrn2N  33604
  Copyright terms: Public domain W3C validator