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

Theorem 3bitr3g 287
Description: More general version of 3bitr3i 275. 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 259 . 2
4 3bitr3g.3 . 2
53, 4syl6bb 261 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  notbid  294  cador  1458  equequ2  1799  dfsbcq2  3330  unineq  3747  iindif2  4399  reusv2  4658  rabxfrd  4673  opeqex  4743  eqbrrdv  5105  eqbrrdiv  5106  opelco2g  5175  opelcnvg  5187  ralrnmpt  6040  fliftcnv  6209  eusvobj2  6289  ottpos  6984  smoiso  7052  ercnv  7351  ordiso2  7961  cantnfrescl  8116  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1OLD  8152  cnfcom  8165  cnfcom3lem  8168  cnfcomOLD  8173  cnfcom3lemOLD  8176  carden2  8389  cardeq0  8948  axpownd  8999  fpwwe2lem9  9037  fzen  11732  hasheq0  12433  incexc2  13650  divalglem4  14054  divalglem8  14058  divalgb  14062  divalgmod  14064  sadadd  14117  sadass  14121  smuval2  14132  smumul  14143  isprm3  14226  vdwmc  14496  imasleval  14938  acsfn2  15060  invsym2  15157  yoniso  15554  pmtrfmvdn0  16487  dprd2d2  17093  cmpfi  19908  xkoinjcn  20188  tgpconcomp  20611  iscau3  21717  mbfimaopnlem  22062  ellimc3  22283  eldv  22302  eltayl  22755  atandm3  23209  el2wlkonot  24869  el2spthonot  24870  rmoxfrdOLD  27391  rmoxfrd  27392  opeldifid  27456  2ndpreima  27525  f1od2  27547  ordtconlem1  27906  wl-dral1d  29984  wl-sb8et  30001  wl-equsb3  30004  wl-sb8eut  30022  wl-ax11-lem8  30032  eqbrrdv2  30604  radcnvrat  31195  aacllem  33216  trsbc  33311  bnj1253  34073  islpln5  35259  islvol5  35303
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 185
  Copyright terms: Public domain W3C validator