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

Theorem 3expb 1154
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expb  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem 3expb
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1152 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 423 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3adant3r1  1162  3adant3r2  1163  3adant3r3  1164  3adant1l  1176  3adant1r  1177  mp3an1  1266  sotri  5261  fnfco  5609  mpt2eq3dva  6138  fovrnda  6217  grprinvd  6286  oaass  6804  omlimcl  6821  odi  6822  nnmsucr  6868  cflim2  8143  mulcanenq  8837  mul4  9235  add4  9281  2addsub  9319  addsubeq4  9320  subadd4  9345  muladd  9466  ltleadd  9511  divmul  9681  divne0  9690  div23  9697  div12  9700  divsubdir  9710  divcan5  9716  divmuleq  9719  divcan6  9721  divdiv32  9722  div2sub  9839  letrp1  9852  lemul12b  9867  lediv1  9875  lt2mul2div  9886  lemuldiv  9889  ltdiv2  9895  ledivdiv  9899  lediv2  9900  ltdiv23  9901  lediv23  9902  sup2  9964  cju  9996  nndivre  10035  nndivtr  10041  nn0addge1  10266  nn0addge2  10267  peano2uz2  10357  uzind  10361  uzind3  10363  fzind  10368  fnn0ind  10369  uzind4  10534  qre  10579  irrmul  10599  rpdivcl  10634  rerpdivcl  10639  xrinfmsslem  10886  ixxin  10933  iccshftr  11030  iccshftl  11032  iccdil  11034  icccntr  11036  fzaddel  11087  fzrev  11108  modlt  11258  modcyc  11276  axdc4uzlem  11321  expdiv  11430  swrd00  11765  swrdcl  11766  2shfti  11895  isermulc2  12451  fsummulc2  12567  dvdscmulr  12878  dvdsmulcr  12879  dvds2add  12881  dvds2sub  12882  dvdstr  12883  alzdvds  12899  divalg2  12925  dvdslegcd  13016  isprm6  13109  pcqcl  13230  vdwmc2  13347  ressinbas  13525  isposd  14412  pleval2i  14421  tosso  14465  clatl  14543  poslubmo  14573  mndplusf  14706  mndfo  14720  imasmnd2  14732  issubm2  14749  0mhm  14758  resmhm  14759  resmhm2  14760  resmhm2b  14761  mhmco  14762  mhmima  14763  submacs  14765  prdspjmhm  14766  pwsdiagmhm  14768  pwsco1mhm  14769  pwsco2mhm  14770  gsumwsubmcl  14784  gsumccat  14787  gsumwmhm  14790  grpinvcnv  14859  grpinvnzcl  14863  grpsubf  14868  mulgnnsubcl  14902  mulgnndir  14912  imasgrp2  14933  divsgrp2  14936  issubg4  14961  isnsg3  14974  nsgacs  14976  nsgid  14986  divsadd  14997  ghmmhm  15016  ghmmhmb  15017  idghm  15021  resghm  15022  ghmf1  15034  divsghm  15042  gaid  15076  subgga  15077  gasubg  15079  invoppggim  15156  lsmidm  15296  pj1ghm  15335  mulgnn0di  15448  mulgmhm  15450  mulgghm  15451  invghm  15453  ghmplusg  15461  ablnsg  15462  divsabl  15480  gsumval3eu  15513  gsumval3  15514  gsumzcl  15518  gsumzaddlem  15526  gsumzadd  15527  gsumzmhm  15533  gsumzoppg  15539  rnglghm  15711  rngrghm  15712  issubrg2  15888  issrngd  15949  islmodd  15956  lmodscaf  15972  lmodvsghm  16005  lssacs  16043  idlmhm  16117  invlmhm  16118  lmhmvsca  16121  reslmhm2  16129  reslmhm2b  16130  pwsdiaglmhm  16133  issubrngd2  16262  divsrhm  16308  crngridl  16309  divscrng  16311  isnzr2  16334  domnmuln0  16358  opprdomn  16361  asclghm  16397  asclrhm  16400  psraddcl  16447  psrvscacl  16457  psrass23  16473  psrbagev1  16566  coe1sclmulfv  16675  expmhm  16776  zntoslem  16837  znfld  16841  phlipf  16883  tgclb  17035  topbas  17037  ntrss  17119  mretopd  17156  neissex  17191  cnpnei  17328  lmcnp  17368  ordthaus  17448  llynlly  17540  restnlly  17545  llyidm  17551  nllyidm  17552  ptbasin  17609  txcnp  17652  ist0-4  17761  kqt0lem  17768  isr0  17769  regr1lem2  17772  cmphmph  17820  conhmph  17821  fbun  17872  trfbas2  17875  isfil2  17888  isfild  17890  infil  17895  fbasfip  17900  fbasrn  17916  trfil2  17919  rnelfmlem  17984  fmfnfmlem3  17988  flimopn  18007  txflf  18038  fclsnei  18051  fclsfnflim  18059  fcfnei  18067  clssubg  18138  tgphaus  18146  divstgplem  18150  tsmsadd  18176  psmetxrge0  18344  psmetlecl  18346  xmetlecl  18376  xmettpos  18379  imasdsf1olem  18403  imasf1oxmet  18405  imasf1omet  18406  elbl3ps  18421  elbl3  18422  metss  18538  comet  18543  stdbdxmet  18545  stdbdmet  18546  methaus  18550  nrmmetd  18622  abvmet  18623  isngp4  18658  subgngp  18676  nmoi2  18764  nmoleub  18765  nmoid  18776  bl2ioo  18823  zcld  18844  divcn  18898  divccn  18903  cncffvrn  18928  divccncf  18936  icoopnst  18964  clmzlmvsca  19121  cph2ass  19175  tchcph  19194  cfilfcls  19227  bcthlem2  19278  cldcss  19342  dvrec  19841  dvmptfsum  19859  aalioulem3  20251  taylply2  20284  dchrelbasd  21023  dchrmulcl  21033  pntrmax  21258  padicabv  21324  usgraidx2vlem1  21410  usgraidx2vlem2  21411  grpoidinvlem2  21793  grpoidinvlem3  21794  grponpncan  21843  ablo4  21875  ablomuldiv  21877  gxdi  21884  ghgrp  21956  ghsubgolem  21958  efghgrp  21961  nvaddsub4  22142  nvmeq0  22145  nvelbl  22185  nvelbl2  22186  sspmval  22232  sspival  22237  sspimsval  22239  lnosub  22260  dipsubdir  22349  sspph  22356  hvadd4  22538  hvpncan  22541  his35  22590  hiassdi  22593  shscli  22819  shmodsi  22891  chj4  23037  spansnmul  23066  spansncol  23070  spanunsni  23081  hoadd4  23287  hosubadd4  23317  lnopl  23417  unopf1o  23419  counop  23424  lnfnl  23434  hmopadj2  23444  eighmre  23466  lnopmi  23503  lnophsi  23504  hmops  23523  hmopm  23524  cnlnadjlem2  23571  adjmul  23595  adjadd  23596  kbass6  23624  mdslj1i  23822  mdslj2i  23823  mdslmd1lem1  23828  mdslmd2i  23833  chirredlem3  23895  isoun  24089  xdivmul  24171  isarchi2  24255  metider  24289  ismeas  24553  dya2iocnei  24632  cnpcon  24917  cvmseu  24963  ghomf1olem  25105  subdivcomb1  25195  axsegconlem1  25856  axlowdimlem15  25895  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  cnambfre  26255  itg2addnclem2  26257  ftc1anclem5  26284  ftc1anclem6  26285  fneint  26357  fnessref  26373  tailfb  26406  fzadd2  26445  metf1o  26461  isbnd3b  26494  equivbnd  26499  heiborlem3  26522  rrnmet  26538  rrndstprj1  26539  rrntotbnd  26545  exidcl  26551  ghomco  26558  ghomdiv  26559  grpokerinj  26560  rngoneglmul  26567  rngonegrmul  26568  rngosubdi  26569  rngosubdir  26570  isdrngo2  26574  rngohomco  26590  rngoisocnv  26597  riscer  26604  crngm4  26613  crngohomfo  26616  idlsubcl  26633  inidl  26640  keridl  26642  ispridlc  26680  pridlc3  26683  dmncan1  26686  lcomf  26746  ismrc  26755  isnacs3  26764  mzpindd  26803  pellex  26898  monotoddzzfi  27005  lermxnn0  27015  rmyeq0  27018  rmyeq  27019  lermy  27020  jm2.27  27079  lsmfgcl  27149  pwssplit2  27166  pwssplit3  27167  frlmup1  27227  fsumcnsrcl  27348  rngunsnply  27355  psgnghm  27414  mndvcl  27423  isdomn3  27500  ofdivrec  27520  ofdivcan4  27521  fmulcl  27687  swrdccat  28216  2cshw1lem1  28248  3cyclfrgrarn  28403  frgrawopreg  28438  chordthmALT  29045  bnj563  29111  lflvscl  29875  3dim0  30254  linepsubN  30549  cdlemg2fvlem  31391  trlcoat  31520  istendod  31559  dva1dim  31782  dvhvaddcomN  31894  dihf11  32065  dihlatat  32135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator