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

Theorem 3bitr3g 316
Description: More general version of 3bitr3i 304. 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, 2bitr3id 288 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3g.3 . 2 (𝜒𝜏)
53, 4syl6bb 290 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  notbid  321  cador  1610  cbvexdvaw  2047  cbvexdw  2361  cbvexd  2431  cbvrexdva2OLD  3443  vtoclgft  3539  dfsbcq2  3761  unineq  4239  iindif2  4985  reusv2  5291  rabxfrd  5305  opeqex  5375  eqbrrdv  5653  eqbrrdiv  5654  opelco2g  5725  opelcnvg  5738  ralrnmptw  6851  ralrnmpt  6853  fliftcnv  7057  eusvobj2  7142  br1steqg  7706  br2ndeqg  7707  ottpos  7898  smoiso  7995  ercnv  8306  ordiso2  8976  cantnfrescl  9136  cantnfp1lem3  9140  cantnflem1b  9146  cantnflem1  9149  cnfcom  9160  cnfcom3lem  9163  djulf1o  9338  djurf1o  9339  carden2  9413  cardeq0  9972  axpownd  10021  fpwwe2lem9  10058  fzen  12928  hasheq0  13729  incexc2  15193  divalglem4  15745  divalglem8  15749  divalgb  15753  sadadd  15814  sadass  15818  smuval2  15829  smumul  15840  isprm3  16025  vdwmc  16312  imasleval  16814  acsfn2  16934  invsym2  17033  yoniso  17535  pmtrfmvdn0  18590  dprd2d2  19166  cmpfi  22016  xkoinjcn  22295  tgpconncomp  22721  iscau3  23885  mbfimaopnlem  24262  ellimc3  24485  eldv  24504  eltayl  24958  atandm3  25467  rmoxfrd  30266  opeldifid  30360  2ndpreima  30454  f1od2  30468  ordtconnlem1  31224  bnj1253  32346  usgrgt2cycl  32434  satfdm  32673  noetalem3  33276  wl-dral1d  34881  wl-sb8et  34899  wl-equsb3  34902  wl-sb8eut  34923  wl-ax11-lem8  34934  wl-clelsb3df  34973  poimirlem2  35004  poimirlem16  35018  poimirlem18  35020  poimirlem21  35023  poimirlem22  35024  eqbrrdv2  36104  islpln5  36776  islvol5  36820  ntrneicls11  40712  radcnvrat  40938  trsbc  41166  ichnreuop  43915  ichreuopeq  43916  aacllem  45255
  Copyright terms: Public domain W3C validator