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

Theorem 3bitr3i 267
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 243 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 241 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  an12  773  cadan  1401  19.35  1610  cbval2  1989  cbval2OLD  1990  cbvex2  1991  sbco2d  2162  equsb3  2178  elsb3  2179  elsb4  2180  sbcom2  2190  sb7f  2196  eq2tri  2495  eqsb3  2537  clelsb3  2538  r19.35  2855  ralcom4  2974  rexcom4  2975  ceqsralt  2979  gencbvex  2998  gencbval  3000  ceqsrexbv  3070  euind  3121  reuind  3137  sbccomlem  3231  sbccom  3232  difcom  3712  uniintsn  4087  disjxun  4210  exss  4426  reusv2lem4  4727  elxp2  4896  eqbrriv  4971  dm0rn0  5086  dfres2  5193  qfto  5255  rninxp  5310  fununi  5517  dffv2  5796  fndmin  5837  dfoprab2  6121  dfer2  6906  eceqoveq  7009  euen1  7177  xpsnen  7192  xpassen  7202  marypha2lem3  7442  rankuni  7789  card1  7855  alephislim  7964  dfacacn  8021  kmlem4  8033  ac6num  8359  zorn2lem4  8379  fpwwe2lem8  8512  fpwwe2lem12  8516  mappsrpr  8983  sqeqori  11493  vdwmc2  13347  txflf  18038  metustidOLD  18589  metustid  18590  caucfil  19236  ovolgelb  19376  nmoubi  22273  hvsubaddi  22568  hlimeui  22743  omlsilem  22904  pjoml3i  23088  hodsi  23278  nmopub  23411  nmfnleub  23428  nmopcoadj0i  23606  pjin3i  23697  or3dir  23952  ralcom4f  23965  rexcom4f  23966  clelsb3f  23971  br1steq  25398  br2ndeq  25399  elima4  25404  brfullfun  25793  axcontlem5  25907  filnetlem4  26410  moxfr  26733  coeq0  26810  pm11.6  27568  cbvexsv  28633  bnj62  29085  bnj610  29115  bnj1143  29161  bnj1533  29223  bnj543  29264  bnj545  29266  bnj594  29283  sbco2dwAUX7  29586  equsb3NEW7  29602  elsb3NEW7  29603  elsb4NEW7  29604  sbcom2NEW7  29644  cbval2OLD7  29730  cbvex2OLD7  29731  sbco2dOLD7  29753  dfsb7OLD7  29763  sb7fOLD7  29764  isltrn2N  30917
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator