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

Theorem 3bitr3g 300
Description: More general version of 3bitr3i 288. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
Hypotheses
Ref Expression
3bitr3g.1 (𝜑 → (𝜓𝜒))
3bitr3g.2 (𝜓𝜃)
3bitr3g.3 (𝜒𝜏)
Assertion
Ref Expression
3bitr3g (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr3g
StepHypRef Expression
1 3bitr3g.2 . . 3 (𝜓𝜃)
2 3bitr3g.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5bbr 272 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4syl6bb 274 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  notbid  306  cador  1537  equequ2OLD  1941  cbvexdva  2270  dfsbcq2  3404  unineq  3835  iindif2  4519  reusv2  4795  rabxfrd  4810  opeqex  4881  eqbrrdv  5129  eqbrrdiv  5130  opelco2g  5199  opelcnvg  5212  ralrnmpt  6261  fliftcnv  6439  eusvobj2  6520  ottpos  7226  smoiso  7323  ercnv  7627  ordiso2  8280  cantnfrescl  8433  cantnfp1lem3  8437  cantnflem1b  8443  cantnflem1  8446  cnfcom  8457  cnfcom3lem  8460  carden2  8673  cardeq0  9230  axpownd  9279  fpwwe2lem9  9316  fzen  12184  hasheq0  12967  incexc2  14355  divalglem4  14903  divalglem8  14907  divalgb  14911  divalgmodOLD  14914  sadadd  14973  sadass  14977  smuval2  14988  smumul  14999  isprm3  15180  vdwmc  15466  imasleval  15970  acsfn2  16093  invsym2  16192  yoniso  16694  pmtrfmvdn0  17651  dprd2d2  18212  cmpfi  20963  xkoinjcn  21242  tgpconcomp  21668  iscau3  22802  mbfimaopnlem  23145  ellimc3  23366  eldv  23385  eltayl  23835  atandm3  24322  el2wlkonot  26162  el2spthonot  26163  rmoxfrdOLD  28522  rmoxfrd  28523  opeldifid  28600  2ndpreima  28674  f1od2  28693  ordtconlem1  29104  bnj1253  30145  wl-dral1d  32293  wl-sb8et  32309  wl-equsb3  32312  wl-sb8eut  32334  wl-ax11-lem8  32344  poimirlem2  32377  poimirlem16  32391  poimirlem18  32393  poimirlem21  32396  poimirlem22  32397  eqbrrdv2  32962  islpln5  33635  islvol5  33679  ntrneicls11  37204  radcnvrat  37331  trsbc  37567  aacllem  42312
  Copyright terms: Public domain W3C validator