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

Theorem 3bitr4g 288
Description: More general version of 3bitr4i 277. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)
Hypotheses
Ref Expression
3bitr4g.1
3bitr4g.2
3bitr4g.3
Assertion
Ref Expression
3bitr4g

Proof of Theorem 3bitr4g
StepHypRef Expression
1 3bitr4g.2 . . 3
2 3bitr4g.1 . . 3
31, 2syl5bb 257 . 2
4 3bitr4g.3 . 2
53, 4syl6bbr 263 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  bibi1d  319  pm5.32rd  640  orbi2d  701  orbi1d  702  3orbi123d  1298  3anbi123d  1299  nanbi1  1354  nanbi2  1355  xorbi12d  1377  hadbi123d  1449  cadbi123d  1450  cad1  1465  had0  1471  nfbidf  1887  cbvexd  2026  drex1  2069  drnf1  2071  drsb1  2118  eujustALT  2285  eubid  2302  mobid  2303  eqeq1d  2459  eqeq1dALT  2460  eqeq1OLD  2462  eqeq2d  2471  eqeq2OLD  2473  eleq1d  2526  eleq2d  2527  eleq2dALT  2528  eleq1OLD  2531  eleq2OLD  2532  nfceqdf  2614  drnfc1  2638  drnfc2  2639  neeq1OLD  2739  neeq2OLD  2741  neleq12d  2794  neleq1OLD  2796  neleq2OLD  2798  r19.21t  2854  r19.21tOLD  2855  ralbida  2890  ralbidv2  2892  r19.23t  2935  rexbida  2963  rexbidv2  2964  ralcom2  3022  reubida  3040  rmobida  3045  raleqf  3050  rexeqf  3051  reueq1f  3052  rmoeq1f  3053  cbvraldva2  3088  cbvrexdva2  3089  dfsbcq  3329  sbceqbid  3334  sbcbi2  3378  sbcbid  3385  sbcrextOLD  3409  sbcrext  3410  sbcabel  3416  psseq1  3590  psseq2  3591  ssconb  3636  uneq1  3650  ineq1  3692  difin2  3759  reuun2  3780  sbcnel12g  3826  sbnfc2  3854  reldisj  3870  undif4  3883  disjssun  3884  pssdifcom1  3913  pssdifcom2  3914  sbcssg  3940  eltpg  4071  raltpg  4080  rextpg  4081  r19.12sn  4095  intmin4  4316  dfiun2g  4362  iindif2  4399  iinin2  4400  disjprg  4448  disjxun  4450  breq  4454  breq1  4455  breq2  4456  treq  4551  reusv2lem5  4657  reusv5OLD  4662  reusv7OLD  4664  rexxfrd  4667  rexxfr2d  4669  rabxfrd  4673  opthg2  4729  oteqex2  4744  oteqex  4745  poeq1  4808  soeq1  4824  freq1  4854  weeq1  4872  weeq2  4873  ordeq  4890  limeq  4895  ordunisssuc  4985  opthprc  5052  wesn  5076  releq  5090  sbcrel  5094  eqrel  5097  eqrelrel  5109  xpiindi  5143  brcnvg  5188  brresg  5287  resieq  5289  dmsnopg  5484  dfco2a  5512  iotaeq  5564  sniota  5583  sbcfung  5616  imadif  5668  fneq1  5674  fneq2  5675  feq1  5718  feq2  5719  feq3  5720  sbcfng  5733  sbcfg  5734  f1eq1  5781  f1eq2  5782  f1eq3  5783  foeq1  5796  foeq2  5797  foeq3  5798  f1oeq1  5812  f1oeq2  5813  f1oeq3  5814  mpteqb  5970  rexrnmpt  6041  dffo3  6046  fmptco  6064  dff13  6166  f1imaeq  6173  f1imapss  6174  cbvexfo  6193  f1eqcocnv  6204  fliftcnv  6209  isoeq1  6215  isoeq2  6216  isoeq3  6217  isoeq4  6218  isoeq5  6219  isomin  6233  isowe  6245  fnotovb  6338  mpt2eq123  6356  rexrnmpt2  6418  iunpw  6614  tfinds  6694  fun11iun  6760  opiota  6859  ottpos  6984  dmtpos  6986  onoviun  7033  smoeq  7040  smoiso2  7059  tfr2b  7084  oarec  7230  oeeui  7270  nnacan  7296  nnmcan  7302  ereq1  7337  ereq2  7338  elecg  7369  ereldm  7374  ixpiin  7515  boxriin  7531  boxcutc  7532  omxpenlem  7638  nnsdomo  7732  enfi  7756  isfinite2  7798  ixpfi2  7838  elfi2  7894  fipwss  7909  ennum  8349  cardsdom2  8390  aleph11  8486  alephiso  8500  fin23lem26  8726  compssiso  8775  isf34lem4  8778  isfin5-2  8792  fin1a2lem5  8805  brdom7disj  8930  brdom6disj  8931  fpwwe2lem8  9036  fpwwe2lem12  9040  fpwwe2lem13  9041  genpass  9408  ltasr  9498  axpre-lttri  9563  infm3  10527  creur  10555  eqreznegel  11196  rpneg  11278  ltxr  11353  icoshftf1o  11672  elfzm11  11778  elfzomelpfzo  11914  nn0ennn  12089  nnesq  12290  hashbclem  12501  hashf1lem1  12504  leiso  12508  fz1isolem  12510  pr2pwpr  12520  repsdf2  12750  rexfiuz  13180  cau4  13189  ello1mpt2  13345  o1lo1  13360  fsumcom2  13589  incexc2  13650  fprodcom2  13788  bitsmod  14086  bitscmp  14088  smueqlem  14140  hashdvds  14305  prmreclem2  14435  vdwapun  14492  vdwmc2  14497  imasaddfnlem  14925  comfeq  15101  oppcsect  15168  funcres2b  15266  funcpropd  15269  fullpropd  15289  fthpropd  15290  fthres2b  15299  fthres2c  15300  fullres2c  15308  ffthres2c  15309  fucsect  15341  fucinv  15342  setcsect  15416  tosso  15666  pospropd  15764  odulatb  15773  oduclatb  15774  isipodrs  15791  odudlatb  15826  issgrpv  15913  issgrpn0  15914  mndpropd  15946  mhmpropd  15972  issubm2  15979  grppropd  16068  grpinvcnv  16106  conjghm  16297  conjnmzb  16301  ghmpropd  16304  gapm  16344  symg1bas  16421  pmtrfrn  16483  cmnpropd  16807  ablpropd  16808  eqgabl  16843  gsumcom2  17003  dmdprd  17029  dprdw  17043  dprdwOLD  17050  subgdmdprd  17081  pgpfac1lem2  17126  pgpfac1lem4  17129  ringpropd  17230  crngpropd  17231  crngunit  17311  unitpropd  17346  isnirred  17349  drngpropd  17423  fldpropd  17424  subrgpropd  17463  rhmpropd  17464  abvpropd  17491  lmodprop2d  17572  lsspropd  17663  lmhmpropd  17719  lbspropd  17745  lvecprop2d  17812  lvecpropd  17813  rrgsuppOLD  17940  opprdomn  17950  fiidomfld  17957  assapropd  17976  psrbagconf1o  18026  mplmonmul  18126  phlpropd  18690  mat1dimbas  18974  eltopspOLD  19419  istps2OLD  19422  tpspropd  19441  tgss2  19489  lmbr2  19760  ist1-2  19848  ist1-3  19850  subislly  19982  dissnlocfin  20030  iskgen3  20050  txcnmpt  20125  hausdiag  20146  hauseqlcld  20147  xkococnlem  20160  tgqtop  20213  txhmeo  20304  uffix2  20425  ufildr  20432  txflf  20507  tgphaus  20615  qustgplem  20619  qustgphaus  20621  xpsdsval  20884  blin  20924  blres  20934  xmeterval  20935  xmspropd  20976  mspropd  20977  setsms  20983  metequiv  21012  metustsymOLD  21064  metustsym  21065  restmetu  21090  ngppropd  21151  xrtgioo  21311  metdsge  21353  icopnfcnv  21442  iccpnfcnv  21444  lmhmclm  21586  lmmbr  21697  equivcmet  21754  cmspropd  21788  iunmbl2  21967  ioombl1lem4  21971  mbfaddlem  22067  i1fmullem  22101  itg1mulc  22111  iblcnlem1  22194  iblrelem  22197  iblre  22200  iblcn  22205  limcun  22299  mvth  22393  ofmulrt  22678  resinf1o  22923  quad2  23170  1cubr  23173  dcubic  23177  wilthlem2  23343  dvdsflip  23458  dvdsflf1o  23463  dvdsflsumcom  23464  fsumvma  23488  vmasum  23491  logfac2  23492  logfaclbnd  23497  dchrelbas3  23513  lgsquadlem1  23629  lgsquadlem2  23630  ax5seg  24241  clwwlknscsh  24819  el2wlkonotot1  24874  2pthwlkonot  24885  rusgranumwlkb0  24953  eupath2lem2  24978  usg2spot2nb  25065  numclwwlkovfel2  25083  isass  25318  ocin  26214  chpsscon3  26421  chscllem2  26556  adjval  26809  pjimai  27095  mdsldmd1i  27250  elat2  27259  mdsymi  27330  sbceqbidf  27380  rmoxfrdOLD  27391  rmoxfrd  27392  disjrdx  27450  eqrelrd2  27467  fmptcof2  27502  ofpreima  27507  funcnv5mpt  27511  1stpreima  27524  2ndpreima  27525  fpwrelmapffslem  27555  locfinreflem  27843  zhmnrg  27948  qqhval2  27963  ismntop  28004  dfrtrclrec2  29066  dfpo2  29184  dfres3  29188  sscoid  29563  dfrdg4  29600  altopthbg  29618  broutsideof3  29776  wl-sb8eut  30022  wl-sb8mot  30023  ftc1anclem5  30094  istotbnd3  30267  sstotbnd  30271  heibor  30317  isidlc  30412  smprngopr  30449  mrefg2  30639  jm2.23  30938  wepwsolem  30987  dnwech  30994  islssfg2  31017  gicabl  31047  acsfn1p  31148  isdomn3  31164  ralbidar  31354  rexbidar  31355  iccintsng  31563  dfateq12d  32214  aov0nbovbi  32280  fnotaovb  32283  rexxfrd2  32304  mgmhmpropd  32473  rngcsect  32788  rngcsectOLD  32800  ringcsect  32839  ringcsectOLD  32863  lindslinindsimp2lem5  33063  trsbc  33311  bnj919  33825  bnj956  33835  bnj976  33836  bnj1366  33888  bnj916  33991  bj-nfbi  34217  bj-cbvexdv  34301  bj-drex1v  34327  bj-drnf1v  34328  bj-eleq1w  34422  bj-eleq2w  34423  islshpsm  34705  lcvexchlem1  34759  opcon1b  34923  isat3  35032  glbconN  35101  cdleme32fva  36163  cdlemg2cex  36317  dibelval3  36874  dib1dim  36892  doch11  37100  dochsordN  37101  mapdordlem1a  37361  mapd11  37366  mapdsord  37382  mapdcnv11N  37386  mapd0  37392  bj-ifbi1  37699  bj-ifbi2  37700  bj-ifbi3  37701  bj-ifbi12  37702  bj-ifbi13  37703  bj-ifbi23  37704  bj-ifbi123  37705  pwinfig  37746  intimag  37770  heeq12  37800
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