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  xorass  1366  19.35OLD  1693  cbval2  2032  sbco2d  2161  sbcom  2163  equsb3  2178  equsb3ALT  2179  elsb3  2180  elsb4  2181  sb7f  2199  sbco4lem  2211  eq2tri  2522  eqsb3  2574  clelsb3  2575  r19.35  3001  ralcom4  3125  rexcom4  3126  ceqsralt  3130  gencbvex  3150  gencbval  3152  ceqsrexbv  3231  euind  3283  reuind  3300  sbccomlem  3395  sbccom  3396  csbcom  3833  difcom  3900  uniintsn  4309  disjxun  4437  reusv2lem4  4641  exss  4700  elxp2  5006  eqbrriv  5086  dm0rn0  5208  dfres2  5314  qfto  5376  rninxp  5431  coeq0  5499  fununi  5636  dffv2  5921  fndmin  5970  fnprb  6106  dfoprab2  6316  dfer2  7304  eceqoveq  7408  euen1  7578  xpsnen  7594  xpassen  7604  marypha2lem3  7889  rankuni  8272  card1  8340  alephislim  8455  dfacacn  8512  kmlem4  8524  ac6num  8850  zorn2lem4  8870  fpwwe2lem8  9004  fpwwe2lem12  9008  mappsrpr  9474  sqeqori  12265  trclublem  12916  vdwmc2  14584  txflf  20676  metustidOLD  21231  metustid  21232  caucfil  21891  ovolgelb  22060  axcontlem5  24476  nmoubi  25888  hvsubaddi  26184  hlimeui  26359  omlsilem  26521  pjoml3i  26705  hodsi  26895  nmopub  27028  nmfnleub  27045  nmopcoadj0i  27223  pjin3i  27314  or3dir  27569  ralcom4f  27576  rexcom4f  27577  clelsb3f  27580  uniinn0  27633  ordtconlem1  28144  br1steq  29447  br2ndeq  29448  elima4  29452  brfullfun  29829  filnetlem4  30442  sbccom2lem  30772  moxfr  30867  hashnzfzclim  31471  pm11.6  31542  fprodle  31846  copisnmnd  32888  sbc3or  33708  cbvexsv  33732  bnj62  34193  bnj610  34224  bnj1143  34269  bnj1533  34330  bnj543  34371  bnj545  34373  bnj594  34390  bj-cbval2v  34722  bj-clelsb3  34844  isltrn2N  36260  ifporcor  38149  ifpnorcor  38150  ifpancor  38155  ifpnancor  38156  ifpbicor  38162  relexp0eq  38239
  Copyright terms: Public domain W3C validator