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

Theorem 3bitr3i 292
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 268 . 2 (𝜒𝜓)
4 3bitr3i.3 . 2 (𝜓𝜃)
53, 4bitri 266 1 (𝜒𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  xorass  1637  cbvex  2377  cbvexv  2379  cbval2  2382  cbvaldva  2384  sbco2d  2507  sbcom  2509  equsb3  2524  equsb3ALT  2525  elsb3  2527  elsb3OLD  2528  elsb4  2530  elsb4OLD  2531  sb7f  2545  sbco4lem  2557  eq2tri  2826  eqsb3  2871  clelsb3  2872  clelsb3f  2911  r19.35  3231  ralcom4  3377  rexcom4  3378  ceqsralt  3382  gencbvex  3403  gencbval  3405  ceqsrexbv  3490  euind  3552  reuind  3572  sbccomlem  3667  sbccom  3668  csbcom  4155  difcom  4213  eqsn  4514  uniintsn  4670  disjxun  4807  reusv2lem4  5036  exss  5087  opab0  5168  opelinxp  5351  eqbrriv  5384  dm0rn0  5510  elidinxp  5632  qfto  5700  rninxp  5756  coeq0  5830  fununi  6142  dffv2  6460  fndmin  6514  fnprb  6665  fntpb  6666  dfoprab2  6899  dfer2  7948  eceqoveq  8056  euen1  8230  xpsnen  8251  xpassen  8261  marypha2lem3  8550  rankuni  8941  card1  9045  alephislim  9157  dfacacn  9216  kmlem4  9228  ac6num  9554  zorn2lem4  9574  mappsrpr  10182  sqeqori  13183  trclublem  14021  fprodle  15009  vdwmc2  15962  txflf  22089  metustid  22638  caucfil  23360  ovolgelb  23538  dfcgra2  26012  axcontlem5  26139  frgr3v  27555  nmoubi  28083  hvsubaddi  28379  hlimeui  28553  omlsilem  28717  pjoml3i  28901  hodsi  29090  nmopub  29223  nmfnleub  29240  nmopcoadj0i  29418  pjin3i  29509  or3dir  29764  ralcom4f  29772  rexcom4f  29773  uniinn0  29815  ordtconnlem1  30417  bnj62  31237  bnj610  31265  bnj1143  31309  bnj1533  31370  bnj543  31411  bnj545  31413  bnj594  31430  ceqsralv2  32053  brsuccf  32492  brfullfun  32499  filnetlem4  32819  bj-ssbcom3lem  33086  bj-cbval2v  33171  icorempt2  33632  poimirlem13  33846  poimirlem14  33847  poimirlem21  33854  poimirlem22  33855  poimir  33866  sbccom2lem  34350  eldmqsres  34483  alrmomorn  34552  xrninxp2  34580  isltrn2N  36076  moxfr  37933  ifporcor  38482  ifpancor  38484  ifpbicor  38496  ifpnorcor  38501  ifpnancor  38502  ifpororb  38526  relexp0eq  38668  hashnzfzclim  39195  pm11.6  39266  sbc3or  39410  cbvexsv  39425  sprvalpwn0  42402  copisnmnd  42478
  Copyright terms: Public domain W3C validator