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  1435  19.35OLD  1656  cbval2  1987  cbvex2OLD  1989  sbco2d  2123  sbcom  2126  equsb3  2146  equsb3ALT  2147  elsb3  2148  elsb4  2149  sbcom2OLD  2161  sb7f  2172  sbco4lem  2187  eq2tri  2522  eqsb3  2574  clelsb3  2575  r19.35  2971  ralcom4  3095  rexcom4  3096  ceqsralt  3100  gencbvex  3120  gencbval  3122  ceqsrexbv  3199  euind  3251  reuind  3268  sbccomlem  3371  sbccom  3372  csbcom  3796  difcom  3870  uniintsn  4272  disjxun  4397  reusv2lem4  4603  exss  4662  elxp2  4965  eqbrriv  5042  dm0rn0  5163  dfres2  5265  qfto  5326  rninxp  5384  fununi  5591  dffv2  5872  fndmin  5918  fnprb  6044  dfoprab2  6241  dfer2  7211  eceqoveq  7314  euen1  7488  xpsnen  7504  xpassen  7514  marypha2lem3  7797  rankuni  8180  card1  8248  alephislim  8363  dfacacn  8420  kmlem4  8432  ac6num  8758  zorn2lem4  8778  fpwwe2lem8  8914  fpwwe2lem12  8918  mappsrpr  9385  sqeqori  12094  vdwmc2  14157  txflf  19710  metustidOLD  20265  metustid  20266  caucfil  20925  ovolgelb  21094  axcontlem5  23365  nmoubi  24323  hvsubaddi  24619  hlimeui  24794  omlsilem  24956  pjoml3i  25140  hodsi  25330  nmopub  25463  nmfnleub  25480  nmopcoadj0i  25658  pjin3i  25749  or3dir  26004  ralcom4f  26011  rexcom4f  26012  clelsb3f  26015  ordtconlem1  26498  br1steq  27728  br2ndeq  27729  elima4  27733  brfullfun  28122  filnetlem4  28749  moxfr  29175  coeq0  29237  pm11.6  29792  sbc3or  31554  cbvexsv  31572  bnj62  32026  bnj610  32056  bnj1143  32101  bnj1533  32162  bnj543  32203  bnj545  32205  bnj594  32222  bj-cbval2v  32555  bj-clelsb3  32676  isltrn2N  34087
  Copyright terms: Public domain W3C validator