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

Theorem 3bitr3g 302
Description: More general version of 3bitr3i 290. 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 274 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4syl6bb 276 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  notbid  308  cador  1545  equequ2OLD  1953  cbvexdva  2281  dfsbcq2  3432  unineq  3869  iindif2  4580  reusv2  4865  rabxfrd  4880  opeqex  4952  eqbrrdv  5207  eqbrrdiv  5208  opelco2g  5278  opelcnvg  5291  ralrnmpt  6354  fliftcnv  6546  eusvobj2  6628  ottpos  7347  smoiso  7444  ercnv  7748  ordiso2  8405  cantnfrescl  8558  cantnfp1lem3  8562  cantnflem1b  8568  cantnflem1  8571  cnfcom  8582  cnfcom3lem  8585  carden2  8798  cardeq0  9359  axpownd  9408  fpwwe2lem9  9445  fzen  12343  hasheq0  13137  incexc2  14551  divalglem4  15100  divalglem8  15104  divalgb  15108  divalgmodOLD  15111  sadadd  15170  sadass  15174  smuval2  15185  smumul  15196  isprm3  15377  vdwmc  15663  imasleval  16182  acsfn2  16305  invsym2  16404  yoniso  16906  pmtrfmvdn0  17863  dprd2d2  18424  cmpfi  21192  xkoinjcn  21471  tgpconncomp  21897  iscau3  23057  mbfimaopnlem  23403  ellimc3  23624  eldv  23643  eltayl  24095  atandm3  24586  rmoxfrdOLD  29304  rmoxfrd  29305  opeldifid  29384  2ndpreima  29459  f1od2  29473  ordtconnlem1  29944  bnj1253  31059  noetalem3  31839  wl-dral1d  33289  wl-sb8et  33305  wl-equsb3  33308  wl-sb8eut  33330  wl-ax11-lem8  33340  poimirlem2  33382  poimirlem16  33396  poimirlem18  33398  poimirlem21  33401  poimirlem22  33402  eqbrrdv2  33967  islpln5  34640  islvol5  34684  ntrneicls11  38208  radcnvrat  38333  trsbc  38570  aacllem  42312
  Copyright terms: Public domain W3C validator