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

Theorem 3expb 1197
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3expb

Proof of Theorem 3expb
StepHypRef Expression
1 3exp.1 . . 3
213exp 1195 . 2
32imp32 433 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3adant3r1  1205  3adant3r2  1206  3adant3r3  1207  3adant1l  1220  3adant1r  1221  mp3an1  1311  sotri  5399  fnfco  5755  mpt2eq3dva  6361  fovrnda  6446  grprinvd  6514  fnmpt2ovd  6878  offval22  6879  fnsuppres  6946  suppsssn  6954  sprmpt2d  6971  oaass  7229  omlimcl  7246  odi  7247  nnmsucr  7293  cflim2  8664  mulcanenq  9359  mul4  9770  add4  9817  2addsub  9857  addsubeq4  9858  subadd4  9886  muladd  10014  ltleadd  10060  divmul  10235  divne0  10244  div23  10251  div12  10254  divsubdir  10265  divcan5  10271  divmuleq  10274  divcan6  10276  divdiv32  10277  div2sub  10394  letrp1  10409  lemul12b  10424  lediv1  10432  lt2mul2div  10446  lemuldiv  10449  ltdiv2  10455  ledivdiv  10459  lediv2  10460  ltdiv23  10461  lediv23  10462  sup2  10524  cju  10557  nndivre  10596  nndivtr  10602  nn0addge1  10867  nn0addge2  10868  peano2uz2  10975  uzind  10979  uzind3  10981  fzind  10987  fnn0ind  10988  uzind4  11168  qre  11216  irrmul  11236  rpdivcl  11271  rerpdivcl  11276  xrinfmsslem  11528  ixxin  11575  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  fzaddel  11747  fzrev  11771  modlt  12006  modcyc  12031  axdc4uzlem  12092  expdiv  12216  swrd00  12645  swrdcl  12646  swrd0  12658  swrdccat  12718  swrdco  12803  2shfti  12913  isermulc2  13480  fsummulc2  13599  dvdscmulr  14012  dvdsmulcr  14013  dvds2add  14015  dvds2sub  14016  dvdstr  14018  alzdvds  14036  divalg2  14063  dvdslegcd  14154  isprm6  14250  pcqcl  14380  vdwmc2  14497  ressinbas  14693  isposd  15585  pleval2i  15594  tosso  15666  poslubmo  15776  posglbmo  15777  mgmplusf  15881  ismndd  15943  imasmnd2  15957  idmhm  15975  issubm2  15979  0mhm  15989  resmhm  15990  resmhm2  15991  resmhm2b  15992  mhmco  15993  mhmima  15994  submacs  15996  prdspjmhm  15998  pwsdiagmhm  16000  pwsco1mhm  16001  pwsco2mhm  16002  gsumwsubmcl  16006  gsumccat  16009  gsumwmhm  16013  grpinvcnv  16106  grpinvnzcl  16110  grpsubf  16117  mulgnnsubcl  16154  mulgnndir  16164  imasgrp2  16185  qusgrp2  16188  mhmfmhm  16193  issubg4  16220  isnsg3  16235  nsgacs  16237  nsgid  16247  qusadd  16258  ghmmhm  16277  ghmmhmb  16278  idghm  16282  resghm  16283  ghmf1  16295  qusghm  16303  gaid  16337  subgga  16338  gasubg  16340  invoppggim  16395  gsmsymgrfix  16453  lsmidm  16682  pj1ghm  16721  mulgnn0di  16834  mulgmhm  16836  mulgghm  16837  ghmfghm  16839  invghm  16842  ghmplusg  16852  ablnsg  16853  qusabl  16871  gsumval3eu  16907  gsumval3OLD  16908  gsumval3  16911  gsumzcl2  16915  gsumzclOLD  16919  gsumzaddlem  16934  gsumzadd  16935  gsumzaddlemOLD  16936  gsumzaddOLD  16937  gsumzmhm  16957  gsumzmhmOLD  16958  gsumzoppg  16967  gsumzoppgOLD  16968  srgmulgass  17182  srglmhm  17186  srgrmhm  17187  ringlghm  17250  ringrghm  17251  issubrg2  17449  issrngd  17510  islmodd  17518  lmodscaf  17534  lcomf  17548  lmodvsghm  17571  lssacs  17613  idlmhm  17687  invlmhm  17688  lmhmvsca  17691  reslmhm2  17699  reslmhm2b  17700  pwsdiaglmhm  17703  pwssplit2  17706  pwssplit3  17707  issubrngd2  17835  qusrhm  17885  crngridl  17886  quscrng  17888  isnzr2  17911  domnmuln0  17947  opprdomn  17950  asclghm  17987  asclrhm  17991  psraddcl  18036  psrvscacl  18046  psrass23  18065  psrbagev1  18177  psrbagev1OLD  18178  coe1sclmulfv  18324  cply1mul  18335  expmhm  18485  zntoslem  18595  znfld  18599  psgnghm  18616  phlipf  18687  frlmup1  18832  mndvcl  18893  matbas2d  18925  submaeval  19084  minmar1eval  19151  cpmatacl  19217  pmatcollpw1  19277  pmatcollpw  19282  tgclb  19472  topbas  19474  ntrss  19556  mretopd  19593  neissex  19628  cnpnei  19765  lmcnp  19805  ordthaus  19885  llynlly  19978  restnlly  19983  llyidm  19989  nllyidm  19990  ptbasin  20078  txcnp  20121  ist0-4  20230  kqt0lem  20237  isr0  20238  regr1lem2  20241  cmphmph  20289  conhmph  20290  fbun  20341  trfbas2  20344  isfil2  20357  isfild  20359  infil  20364  fbasfip  20369  fbasrn  20385  trfil2  20388  rnelfmlem  20453  fmfnfmlem3  20457  flimopn  20476  txflf  20507  fclsnei  20520  fclsfnflim  20528  fcfnei  20536  clssubg  20607  tgphaus  20615  qustgplem  20619  tsmsadd  20649  psmetxrge0  20817  psmetlecl  20819  xmetlecl  20849  xmettpos  20852  imasdsf1olem  20876  imasf1oxmet  20878  imasf1omet  20879  elbl3ps  20894  elbl3  20895  metss  21011  comet  21016  stdbdxmet  21018  stdbdmet  21019  methaus  21023  nrmmetd  21095  abvmet  21096  isngp4  21131  subgngp  21149  nmoi2  21237  nmoleub  21238  nmoid  21249  bl2ioo  21297  zcld  21318  divcn  21372  divccn  21377  cncffvrn  21402  divccncf  21410  icoopnst  21439  clmzlmvsca  21596  cph2ass  21659  tchcph  21680  cfilfcls  21713  bcthlem2  21764  rrxmet  21835  rrxdstprj1  21836  cldcss  21856  dvrec  22358  dvmptfsum  22376  aalioulem3  22730  taylply2  22763  efsubm  22938  dchrelbasd  23514  dchrmulcl  23524  pntrmax  23749  padicabv  23815  axtgcont  23866  xmstrkgc  24189  axsegconlem1  24220  axlowdimlem15  24259  usgraidx2vlem1  24391  usgraidx2vlem2  24392  wlknwwlkninj  24711  wwlkextsur  24731  3cyclfrgrarn  25013  frgrawopreg  25049  grpoidinvlem2  25207  grpoidinvlem3  25208  grponpncan  25257  ablo4  25289  ablomuldiv  25291  gxdi  25298  ghgrpOLD  25370  ghsubgolemOLD  25372  efghgrpOLD  25375  nvaddsub4  25556  nvmeq0  25559  nvelbl  25599  nvelbl2  25600  sspmval  25646  sspival  25651  sspimsval  25653  lnosub  25674  dipsubdir  25763  sspph  25770  hvadd4  25953  hvpncan  25956  his35  26005  hiassdi  26008  shscli  26235  shmodsi  26307  chj4  26453  spansnmul  26482  spansncol  26486  spanunsni  26497  hoadd4  26703  hosubadd4  26733  lnopl  26833  unopf1o  26835  counop  26840  lnfnl  26850  hmopadj2  26860  eighmre  26882  lnopmi  26919  lnophsi  26920  hmops  26939  hmopm  26940  cnlnadjlem2  26987  adjmul  27011  adjadd  27012  kbass6  27040  mdslj1i  27238  mdslj2i  27239  mdslmd1lem1  27244  mdslmd2i  27249  chirredlem3  27311  isoun  27520  xdivmul  27621  odutos  27651  isarchi2  27729  archiabllem2  27741  metider  27873  pl1cn  27937  ismeas  28170  dya2iocnei  28253  cnpcon  28675  cvmseu  28721  elmrsubrn  28880  mrsubco  28881  ghomf1olem  29034  subdivcomb1  29105  heicant  30049  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  cnambfre  30063  dvtanlem  30064  itg2addnclem2  30067  ftc1anclem5  30094  ftc1anclem6  30095  fneint  30166  fnessref  30175  tailfb  30195  fzadd2  30234  metf1o  30248  isbnd3b  30281  equivbnd  30286  heiborlem3  30309  rrnmet  30325  rrndstprj1  30326  rrntotbnd  30332  exidcl  30338  ghomco  30345  ghomdiv  30346  grpokerinj  30347  rngoneglmul  30354  rngonegrmul  30355  rngosubdi  30356  rngosubdir  30357  isdrngo2  30361  rngohomco  30377  rngoisocnv  30384  riscer  30391  crngm4  30400  crngohomfo  30403  idlsubcl  30420  inidl  30427  keridl  30429  ispridlc  30467  pridlc3  30470  dmncan1  30473  ismrc  30633  isnacs3  30642  mzpindd  30678  pellex  30771  monotoddzzfi  30878  lermxnn0  30888  rmyeq0  30891  rmyeq  30892  lermy  30893  jm2.27  30950  lsmfgcl  31020  fsumcnsrcl  31115  rngunsnply  31122  isdomn3  31164  lcmgcdlem  31212  lcmgcdeq  31216  nzin  31223  ofdivrec  31231  ofdivcan4  31232  fmulcl  31575  usgedgvadf1lem1  32413  usgedgvadf1ALTlem1  32416  ismgmd  32464  idmgmhm  32476  resmgmhm  32486  resmgmhm2  32487  resmgmhm2b  32488  mgmhmco  32489  mgmhmima  32490  submgmacs  32492  mgmplusgiopALT  32518  cicer  32590  c0mgm  32715  c0mhm  32716  chordthmALT  33733  bnj563  33800  lflvscl  34802  3dim0  35181  linepsubN  35476  cdlemg2fvlem  36320  trlcoat  36449  istendod  36488  dva1dim  36711  dvhvaddcomN  36823  dihf11  36994  dihlatat  37064
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  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator