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

Theorem 3bitr3i 289
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1 (𝜑𝜓)
3bitr3i.2 (𝜑𝜒)
3bitr3i.3 (𝜓𝜃)
Assertion
Ref Expression
3bitr3i (𝜒𝜃)

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3 (𝜑𝜒)
2 3bitr3i.1 . . 3 (𝜑𝜓)
31, 2bitr3i 265 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 263 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  an12  834  xorass  1460  cbval2  2267  cbvaldva  2269  sbco2d  2404  sbcom  2406  equsb3  2420  equsb3ALT  2421  elsb3  2422  elsb4  2423  sb7f  2441  sbco4lem  2453  eq2tri  2671  eqsb3  2715  clelsb3  2716  r19.35  3065  ralcom4  3197  rexcom4  3198  ceqsralt  3202  gencbvex  3223  gencbval  3225  ceqsrexbv  3307  euind  3360  reuind  3378  sbccomlem  3475  sbccom  3476  csbcom  3946  difcom  4005  eqsn  4301  uniintsn  4449  disjxun  4581  reusv2lem4  4798  exss  4858  elxp2OLD  5057  eqbrriv  5138  dm0rn0  5263  dfres2  5372  qfto  5436  rninxp  5492  coeq0  5561  fununi  5878  dffv2  6181  fndmin  6232  fnprb  6377  fntpb  6378  dfoprab2  6599  dfer2  7630  eceqoveq  7740  euen1  7912  xpsnen  7929  xpassen  7939  marypha2lem3  8226  rankuni  8609  card1  8677  alephislim  8789  dfacacn  8846  kmlem4  8858  ac6num  9184  zorn2lem4  9204  fpwwe2lem8  9338  fpwwe2lem12  9342  mappsrpr  9808  sqeqori  12838  trclublem  13582  fprodle  14566  vdwmc2  15521  txflf  21620  metustid  22169  caucfil  22889  ovolgelb  23055  dfcgra2  25521  axcontlem5  25648  nmoubi  27011  hvsubaddi  27307  hlimeui  27481  omlsilem  27645  pjoml3i  27829  hodsi  28018  nmopub  28151  nmfnleub  28168  nmopcoadj0i  28346  pjin3i  28437  or3dir  28692  ralcom4f  28700  rexcom4f  28701  clelsb3f  28704  uniinn0  28749  ordtconlem1  29298  bnj62  30040  bnj610  30071  bnj1143  30115  bnj1533  30176  bnj543  30217  bnj545  30219  bnj594  30236  ceqsralv2  30862  br1steq  30917  br2ndeq  30918  brsuccf  31218  brfullfun  31225  filnetlem4  31546  bj-ssbcom3lem  31839  bj-cbval2v  31924  bj-clelsb3  32042  icorempt2  32375  poimirlem13  32592  poimirlem14  32593  poimirlem21  32600  poimirlem22  32601  poimir  32612  sbccom2lem  33099  isltrn2N  34424  moxfr  36273  ifporcor  36825  ifpancor  36827  ifpbicor  36839  ifpnorcor  36844  ifpnancor  36845  ifpororb  36869  relexp0eq  37012  hashnzfzclim  37543  pm11.6  37614  sbc3or  37759  cbvexsv  37783  frgr3v  41445  copisnmnd  41599
  Copyright terms: Public domain W3C validator