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  788  cadanOLD  1437  19.35  1654  cbval2  1974  cbvex2OLD  1976  sbco2d  2114  sbcom  2117  equsb3  2139  equsb3ALT  2140  elsb3  2141  elsb4  2142  sbcom2OLD  2154  sb7f  2165  sbco4lem  2180  eq2tri  2492  eqsb3  2534  clelsb3  2535  r19.35  2857  ralcom4  2981  rexcom4  2982  ceqsralt  2986  gencbvex  3005  gencbval  3007  ceqsrexbv  3083  euind  3135  reuind  3151  sbccomlem  3253  sbccom  3254  csbcom  3677  difcom  3751  uniintsn  4153  disjxun  4278  reusv2lem4  4484  exss  4543  elxp2  4845  eqbrriv  4922  dm0rn0  5043  dfres2  5146  qfto  5207  rninxp  5265  fununi  5472  dffv2  5752  fndmin  5798  fnprb  5923  dfoprab2  6122  dfer2  7090  eceqoveq  7193  euen1  7367  xpsnen  7383  xpassen  7393  marypha2lem3  7675  rankuni  8058  card1  8126  alephislim  8241  dfacacn  8298  kmlem4  8310  ac6num  8636  zorn2lem4  8656  fpwwe2lem8  8792  fpwwe2lem12  8796  mappsrpr  9263  sqeqori  11962  vdwmc2  14023  txflf  19421  metustidOLD  19976  metustid  19977  caucfil  20636  ovolgelb  20805  axcontlem5  23037  nmoubi  23995  hvsubaddi  24291  hlimeui  24466  omlsilem  24628  pjoml3i  24812  hodsi  25002  nmopub  25135  nmfnleub  25152  nmopcoadj0i  25330  pjin3i  25421  or3dir  25676  ralcom4f  25683  rexcom4f  25684  clelsb3f  25687  ordtconlem1  26208  br1steq  27432  br2ndeq  27433  elima4  27437  brfullfun  27826  filnetlem4  28446  moxfr  28873  coeq0  28935  pm11.6  29490  sbc3or  30959  cbvexsv  30977  bnj62  31432  bnj610  31462  bnj1143  31507  bnj1533  31568  bnj543  31609  bnj545  31611  bnj594  31628  bj-cbval2v  31890  bj-clelsb3  31992  isltrn2N  33358
  Copyright terms: Public domain W3C validator