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

Theorem 3bitr3i 283
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 259 . 2  |-  ( ch  <->  ps )
4 3bitr3i.3 . 2  |-  ( ps  <->  th )
53, 4bitri 257 1  |-  ( ch  <->  th )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
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 190
This theorem is referenced by:  an12  811  xorass  1419  cbval2  2131  sbco2d  2256  sbcom  2258  equsb3  2272  equsb3ALT  2273  elsb3  2274  elsb4  2275  sb7f  2293  sbco4lem  2305  eq2tri  2523  eqsb3  2567  clelsb3  2568  r19.35  2949  ralcom4  3078  rexcom4  3079  ceqsralt  3083  gencbvex  3104  gencbval  3106  ceqsrexbv  3185  euind  3237  reuind  3255  sbccomlem  3350  sbccom  3351  csbcom  3795  difcom  3864  uniintsn  4286  disjxun  4414  reusv2lem4  4621  exss  4677  elxp2  4871  eqbrriv  4949  dm0rn0  5070  dfres2  5176  qfto  5240  rninxp  5295  coeq0  5363  fununi  5671  dffv2  5961  fndmin  6012  fnprb  6147  fntpb  6148  dfoprab2  6364  dfer2  7390  eceqoveq  7494  euen1  7665  xpsnen  7682  xpassen  7692  marypha2lem3  7977  rankuni  8360  card1  8428  alephislim  8540  dfacacn  8597  kmlem4  8609  ac6num  8935  zorn2lem4  8955  fpwwe2lem8  9088  fpwwe2lem12  9092  mappsrpr  9558  sqeqori  12418  trclublem  13108  fprodle  14099  vdwmc2  14978  txflf  21070  metustid  21618  caucfil  22302  ovolgelb  22482  dfcgra2  24920  axcontlem5  25047  nmoubi  26462  hvsubaddi  26768  hlimeui  26942  omlsilem  27104  pjoml3i  27288  hodsi  27477  nmopub  27610  nmfnleub  27627  nmopcoadj0i  27805  pjin3i  27896  or3dir  28151  ralcom4f  28159  rexcom4f  28160  clelsb3f  28165  uniinn0  28212  ordtconlem1  28779  bnj62  29575  bnj610  29606  bnj1143  29651  bnj1533  29712  bnj543  29753  bnj545  29755  bnj594  29772  ceqsralv2  30407  br1steq  30463  br2ndeq  30464  elima4  30470  brsuccf  30757  brfullfun  30764  filnetlem4  31086  bj-ssbcom3lem  31308  bj-cbval2v  31383  bj-clelsb3  31502  icorempt2  31799  poimirlem13  31998  poimirlem14  31999  poimirlem21  32006  poimirlem22  32007  poimir  32018  sbccom2lem  32409  isltrn2N  33730  moxfr  35579  ifporcor  36150  ifpancor  36152  ifpbicor  36164  ifpnorcor  36169  ifpnancor  36170  ifpororb  36194  relexp0eq  36338  hashnzfzclim  36715  pm11.6  36786  sbc3or  36933  cbvexsv  36957  copisnmnd  40082
  Copyright terms: Public domain W3C validator