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

Theorem bitr4d 256
Description: Deduction form of bitr4i 252. (Contributed by NM, 30-Jun-1993.)
Hypotheses
Ref Expression
bitr4d.1
bitr4d.2
Assertion
Ref Expression
bitr4d

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2
2 bitr4d.2 . . 3
32bicomd 201 . 2
41, 3bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3bitr2d  281  3bitr2rd  282  3bitr4d  285  3bitr4rd  286  bianabs  880  3anibar  1164  sbcom3  2153  sbal1  2204  sbal2  2205  rmob2  3432  disjprg  4448  reuhypd  4679  ordsssuc  4969  opbrop  5084  opelresi  5290  iota1  5570  funbrfv2b  5917  dffn5  5918  dmfco  5947  fneqeql  5995  f1ompt  6053  dff13  6166  fliftcnv  6209  soisores  6223  isotr  6232  isoini  6234  caovord3  6488  releldm2  6850  brtpos  6983  tpostpos  6994  oe1m  7213  oawordri  7218  oalimcl  7228  omlimcl  7246  omabs  7315  iserd  7356  qliftel  7413  qliftfun  7415  qliftf  7418  ecopovsym  7432  pw2f1olem  7641  mapen  7701  suppeqfsuppbi  7863  funsnfsupp  7873  mapfien  7887  supisolem  7952  wemapso2OLD  7998  cantnflem1  8129  cantnflem1OLD  8152  mapfienOLD  8159  wemapwe  8160  wemapweOLD  8161  rankr1clem  8259  rankr1c  8260  ranklim  8283  r1pwOLD  8285  r1pwcl  8286  isfin1-2  8786  isfin1-4  8788  fin71num  8798  axdc3lem2  8852  ltmnq  9371  prlem936  9446  ltsosr  9492  ltasr  9498  xrlenlt  9673  ltxrlt  9676  letri3  9691  ne0gt0  9710  subadd  9846  ltsubadd2  10048  lesubadd2  10050  suble  10055  ltsub23  10057  ltaddpos2  10068  ltsubpos  10069  subge02  10093  ltord2  10107  leord2  10108  ltaddsublt  10201  divmul  10235  divmul3  10237  rec11r  10268  ltdiv1  10431  ltdivmul2  10445  ledivmul2  10447  ltrec  10451  ltdiv2  10455  negiso  10544  infmrgelb  10548  infmrlb  10549  nnle1eq1  10589  avgle1  10803  avgle2  10804  avgle  10805  nn0le0eq0  10849  elz2  10906  znnnlt1  10916  zleltp1  10939  uzin  11142  difrp  11282  xrltlen  11381  dfle2  11382  xrletri3  11387  qbtwnre  11427  xltnegi  11444  supxrre  11548  supxrre1  11551  infmxrre  11556  ixxun  11574  elioo5  11611  elfz5  11709  elfzm11  11778  uzsplit  11779  flbi  11952  flbi2  11953  fznnfl  11989  zmodid2  12024  2submod  12048  lt2sq  12241  le2sq  12242  sqlecan  12274  bcval5  12396  shftfib  12905  mulre  12954  cnpart  13073  sqrlem6  13081  sqrmo  13085  elicc4abs  13152  abs2difabs  13167  cau4  13189  limsupgre  13304  clim2  13327  ello12  13339  ello1mpt2  13345  elo12  13350  lo1resb  13387  o1resb  13389  climeq  13390  climmpt2  13396  isercoll  13490  caucvgb  13502  fsumss  13547  fsumabs  13615  isumshft  13651  geomulcvg  13685  fprodss  13755  absefib  13933  xpnnenOLD  13943  dvdsval3  13990  dvdseq  14033  ndvdsadd  14066  bitscmp  14088  smupvallem  14133  dvdssq  14198  isprm3  14226  coprmdvds  14243  isprm5  14253  phiprmpw  14306  prmdiv  14315  pc11  14403  pcz  14404  pockthlem  14423  prmreclem2  14435  prmreclem4  14437  prmreclem6  14439  1arith  14445  vdwapun  14492  ramval  14526  rami  14533  ramcl  14547  pwsle  14889  ercpbllem  14945  invsym  15156  funcres2c  15270  latnle  15715  grpinvcnv  16106  subgacs  16236  eqger  16251  gexdvds2  16605  pgpfi1  16615  pgpfi  16625  lsmass  16688  lssnle  16692  lsmdisj3b  16708  lsmhash  16723  ablsubadd  16822  gsumval3OLD  16908  gsumval3lem2  16910  subgdmdprd  17081  pgpfac1lem2  17126  dvdsr02  17305  drngid2  17412  issubrg3  17457  lssacs  17613  lspsnel5  17641  psrbaglefi  18023  psrbaglefiOLD  18024  coe1mul2lem1  18308  prmirred  18525  prmirredOLD  18528  chrdvds  18565  chrcong  18566  chrnzr  18567  znleval  18593  znleval2  18594  cygznlem3  18608  frlmbas  18786  elfilspd  18838  lindfmm  18862  islindf4  18873  islindf5  18874  mdetunilem9  19122  discld  19590  isneip  19606  neiptopnei  19633  lpdifsn  19644  restopnb  19676  restopn2  19678  restdis  19679  restperf  19685  lmbr2  19760  cncls2  19774  cnprest  19790  cnprest2  19791  iscnrm2  19839  ist0-2  19845  cnt0  19847  ist1-3  19850  ishaus2  19852  cmpfi  19908  dfcon2  19920  1stccnp  19963  1stccn  19964  subislly  19982  hausmapdom  20001  kgencn  20057  tx1cn  20110  tx2cn  20111  txcnmpt  20125  txrest  20132  hauseqlcld  20147  tgqtop  20213  qtopcld  20214  qtopcn  20215  ordthmeolem  20302  trfil2  20388  trfil3  20389  trnei  20393  ufildr  20432  fmfg  20450  rnelfm  20454  fmfnfm  20459  elflim  20472  fbflim  20477  flimrest  20484  isflf  20494  cnflf  20503  cnflf2  20504  fclscf  20526  cnfcf  20543  ptcmplem2  20553  ghmcnp  20613  tsmssubm  20644  iscfilu  20791  xmetgt0  20861  prdsxmetlem  20871  elbl2ps  20892  elbl2  20893  blcomps  20896  blcom  20897  xblpnfps  20898  xblpnf  20899  blpnf  20900  xmeter  20936  setsxms  20982  imasf1obl  20991  stdbdbl  21020  metrest  21027  metcn  21046  txmetcn  21051  metuel2  21082  dscopn  21094  xrtgioo  21311  metdstri  21355  cncffvrn  21402  cnmpt2pc  21428  iihalf2  21433  icopnfhmeo  21443  evth2  21460  lmmbr3  21699  iscau3  21717  lmclimf  21742  metcld  21744  cfilucfil3OLD  21757  cfilucfil3  21758  srabn  21800  rrxmet  21835  minveclem4  21847  evthicc2  21872  ovolfioo  21879  ovolficc  21880  ovolgelb  21891  ovoliun  21916  shft2rab  21919  ovolshftlem1  21920  sca2rab  21923  ovolscalem1  21924  ismbl2  21938  ioombl1lem4  21971  mbfmulc2lem  22054  mbfmax  22056  mbfposr  22059  ismbf3d  22061  mbfaddlem  22067  mbfsup  22071  mbfinf  22072  i1f1lem  22096  i1fmulclem  22109  mbfi1fseqlem4  22125  itg2seq  22149  itg2monolem1  22157  itg2cnlem1  22168  itgfsum  22233  ditgneg  22261  limcdif  22280  limcnlp  22282  cnplimc  22291  rolle  22391  mvth  22393  dvne0  22412  lhop1lem  22414  itgsubst  22450  mdegle0  22477  deg1leb  22495  deg1le0  22512  q1peqb  22555  coemulhi  22651  dgrlt  22663  plydivlem3  22691  vieta1lem2  22707  aannenlem1  22724  ulmres  22783  reefiso  22843  pilem3  22848  ellogdm  23020  root1eq1  23129  angpieqvdlem  23159  angpieqvdlem2  23160  quad2  23170  1cubr  23173  quart  23192  rlimcnp  23295  wilthlem2  23343  sgmss  23380  isppw  23388  dvdsflip  23458  dvdsflsumcom  23464  fsumvma  23488  logfac2  23492  chpchtsum  23494  dchrmulcl  23524  dchreq  23533  dchrresb  23534  bclbnd  23555  bposlem1  23559  bposlem5  23563  lgsneg  23594  lgsquadlem1  23629  lgsquadlem2  23630  m1lgs  23637  dchrisumlem3  23676  dchrisum0lem1  23701  trgcgrg  23906  tgellng  23940  lnrot1  24003  islnopp  24113  ismidb  24144  islmib  24153  ttgelitv  24186  axsegconlem6  24225  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem12  24278  dfconngra1  24671  clwwlkn2  24775  eupath2  24980  frgra3v  25002  drngoi  25409  nmoreltpnf  25684  isblo2  25698  nmlnogt0  25712  phoeqi  25773  ubthlem2  25787  hire  26011  normgt0  26044  ho01i  26747  ho02i  26748  hoeq1  26749  hoeq2  26750  nmopreltpnf  26788  adjeq  26854  leop  27042  leopmul2i  27054  pjnormssi  27087  pjimai  27095  jplem1  27187  mddmd2  27228  mdslmd1lem1  27244  mdslmd1lem2  27245  superpos  27273  atnssm0  27295  dmdbr5ati  27341  disjunsn  27453  fcoinvbr  27461  feqmptdf  27501  ofpreima  27507  funcnv5mpt  27511  isoun  27520  fpwrelmapffslem  27555  fpwrelmap  27556  xgepnf  27570  xlemnf  27571  xrge0infssd  27581  iocinioc2  27590  xrdifh  27591  nndiffz1  27596  xdivmul  27621  isarchi2  27729  fimaproj  27836  sqsscirc2  27891  xrmulc1cn  27912  ismntoplly  28003  esumfsup  28076  1stmbfm  28231  2ndmbfm  28232  mbfmcnt  28239  oms0  28266  eulerpartlems  28299  eulerpartlemd  28305  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsima  28454  ballotlemfrcn0  28468  sgn3da  28480  erdszelem7  28641  erdszelem9  28643  iscvm  28704  cvmlift3lem4  28767  predfz  29283  sltval2  29416  fscgr  29730  seglelin  29766  btwnoutside  29775  lineunray  29797  nndivsub  29922  wl-sbhbt  30002  wl-sbcom2d  30011  wl-sbalnae  30012  wl-ax11-lem8  30032  sin2h  30045  cos2h  30046  ptrest  30048  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2addnclem  30066  itg2addnclem2  30067  itg2gt0cn  30070  iblabsnclem  30078  ftc1anclem6  30095  areacirclem2  30108  areacirclem5  30111  areacirc  30112  cldbnd  30144  isfne4  30158  fneval  30170  filnetlem4  30199  cover2  30204  mettrifi  30250  prter3  30623  fz1eqin  30702  diophin  30706  dvdsabsmod0  30928  divalgmodcl  30929  jm2.19  30935  rmxdiophlem  30957  pw2f1ocnv  30979  wepwsolem  30987  gicabl  31047  sdrgacs  31150  idomodle  31153  isdomn3  31164  radcnvrat  31195  lcmdvds  31214  bcc0  31245  unima  31441  clim2f  31642  2reu4a  32194  dfdfat2  32216  funbrafv2b  32244  dfafn5a  32245  leaddsuble  32319  isfusgracl  32426  lindslinindimp2lem4  33062  snlindsntor  33072  bnj1173  34058  islshpat  34742  lsatnle  34769  ellkr2  34816  lshpkr  34842  lkr0f2  34886  lduallkr3  34887  lkreqN  34895  cvrval2  34999  isat3  35032  glbconN  35101  hlrelat5N  35125  cvrval4N  35138  atlt  35161  1cvrco  35196  pmaple  35485  isline2  35498  isline4N  35501  elpaddn0  35524  elpadd2at2  35531  cdlemkid4  36660  dia0  36779  cdlemm10N  36845  dibglbN  36893  dihmeetlem4preN  37033  dochkrshp3  37115  dvh4dimlem  37170  lcfl5  37223  mapdpglem3  37402  mapdheq  37455  hdmap1eq  37529  hdmapval2lem  37561  hdmapoc  37661  hlhillcs  37688  extoimad  37981
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