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

Theorem 3bitr3i 301
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 277 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 275 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 205
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 206
This theorem is referenced by:  an33rean  1484  xorass  1515  cbvaldvaw  2042  sbievw2  2100  sbco4lem  2273  sbco4lemOLD  2274  cbvexv1  2339  cbvex  2398  sbco2d  2515  sbcom  2517  sb7f  2529  eq2tri  2804  clelsb2OLD  2867  clelsb1fw  2912  clelsb1f  2913  rexcom  3274  cbvrexfw  3289  cbvraldva2  3324  cbvrexdva2OLD  3326  ceqsralt  3477  gencbvex  3505  gencbval  3507  ceqsrexbv  3607  ceqsralbv  3608  euind  3683  reuind  3712  sbccomlem  3827  sbccom  3828  csbcom  4378  difcom  4447  eqsn  4790  uniintsn  4949  disjxun  5104  reusv2lem4  5357  exss  5421  opab0  5512  opelinxp  5712  eqbrriv  5748  dm0rn0  5881  elidinxp  5998  qfto  6076  rninxp  6132  coeq0  6208  fununi  6577  dffv2  6937  fndmin  6996  fnprb  7159  fntpb  7160  dfoprab2  7416  frpoins3xp3g  8074  dfer2  8650  eceqoveq  8762  euen1  8971  xpsnen  9000  xpassen  9011  marypha2lem3  9374  rankuni  9800  card1  9905  alephislim  10020  dfacacn  10078  kmlem4  10090  ac6num  10416  zorn2lem4  10436  mappsrpr  11045  sqeqori  14119  trclublem  14881  fprodle  15880  vdwmc2  16852  txflf  23360  metustid  23913  caucfil  24650  ovolgelb  24847  dfcgra2  27775  axcontlem5  27920  frgr3v  29222  nmoubi  29717  hvsubaddi  30011  hlimeui  30185  omlsilem  30347  pjoml3i  30531  hodsi  30720  nmopub  30853  nmfnleub  30870  nmopcoadj0i  31048  pjin3i  31139  or3dir  31394  ralcom4f  31401  rexcom4f  31402  uniinn0  31472  ordtconnlem1  32508  bnj62  33335  bnj610  33362  bnj1143  33405  bnj1533  33467  bnj543  33508  bnj545  33510  bnj594  33527  cusgracyclt3v  33753  xpab  34300  brsuccf  34529  brfullfun  34536  filnetlem4  34856  icorempo  35825  poimirlem13  36094  poimirlem14  36095  poimirlem21  36102  poimirlem22  36103  poimir  36114  sbccom2lem  36586  alrmomorn  36822  dfeldisj5  37186  mpet2  37305  isltrn2N  38586  moxfr  41018  ifporcor  41741  ifpancor  41743  ifpbicor  41754  ifpnorcor  41759  ifpnancor  41760  ifpororb  41784  minregex  41813  relexp0eq  41980  hashnzfzclim  42609  pm11.6  42679  sbc3or  42821  cbvexsv  42836  dfich2  45657  ichbi12i  45659  sprvalpwn0  45682  copisnmnd  46110
  Copyright terms: Public domain W3C validator