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

Theorem 3expb 1152
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 1150 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 422 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3adant3r1  1160  3adant3r2  1161  3adant3r3  1162  3adant1l  1174  3adant1r  1175  mp3an1  1264  sotri  5086  fnfco  5423  mpt2eq3dva  5928  fovrnda  6007  grprinvd  6075  oaass  6575  omlimcl  6592  odi  6593  nnmsucr  6639  eroprf  6772  cflim2  7905  mulcanenq  8600  mul4  8997  add4  9043  2addsub  9081  addsubeq4  9082  subadd4  9107  muladd  9228  ltleadd  9273  divmul  9443  divne0  9452  div23  9459  div12  9462  divsubdir  9472  divcan5  9478  divmuleq  9481  divcan6  9483  divdiv32  9484  div2sub  9601  letrp1  9614  lemul12b  9629  lediv1  9637  lt2mul2div  9648  lemuldiv  9651  ltdiv2  9657  ledivdiv  9661  lediv2  9662  ltdiv23  9663  lediv23  9664  sup2  9726  cju  9758  nndivre  9797  nndivtr  9803  nn0addge1  10026  nn0addge2  10027  peano2uz2  10115  uzind  10119  uzind3  10121  fzind  10126  fnn0ind  10127  uzind4  10292  qre  10337  irrmul  10357  rpdivcl  10392  rerpdivcl  10397  xrinfmsslem  10642  ixxin  10689  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzaddel  10842  fzrev  10862  modlt  10997  modcyc  11015  axdc4uzlem  11060  expdiv  11168  swrd00  11467  swrdcl  11468  2shfti  11591  isermulc2  12147  fsummulc2  12262  dvdscmulr  12573  dvdsmulcr  12574  dvds2add  12576  dvds2sub  12577  dvdstr  12578  alzdvds  12594  divalg2  12620  dvdslegcd  12711  isprm6  12804  pcqcl  12925  vdwmc2  13042  ressinbas  13220  isposd  14105  pleval2i  14114  tosso  14158  clatl  14236  poslubmo  14266  mndplusf  14399  mndfo  14413  imasmnd2  14425  issubm2  14442  0mhm  14451  resmhm  14452  resmhm2  14453  resmhm2b  14454  mhmco  14455  mhmima  14456  submacs  14458  prdspjmhm  14459  pwsdiagmhm  14461  pwsco1mhm  14462  pwsco2mhm  14463  gsumwsubmcl  14477  gsumccat  14480  gsumwmhm  14483  grpinvcnv  14552  grpinvnzcl  14556  grpsubf  14561  mulgnnsubcl  14595  mulgnndir  14605  imasgrp2  14626  divsgrp2  14629  issubg4  14654  isnsg3  14667  nsgacs  14669  nsgid  14679  divsadd  14690  ghmmhm  14709  ghmmhmb  14710  idghm  14714  resghm  14715  ghmf1  14727  divsghm  14735  gaid  14769  subgga  14770  gass  14771  gasubg  14772  invoppggim  14849  lsmidm  14989  pj1ghm  15028  mulgnn0di  15141  mulgmhm  15143  mulgghm  15144  invghm  15146  ghmplusg  15154  ablnsg  15155  divsabl  15173  gsumval3eu  15206  gsumval3  15207  gsumzcl  15211  gsumzaddlem  15219  gsumzadd  15220  gsumzmhm  15226  gsumzoppg  15232  rnglghm  15404  rngrghm  15405  issubrg2  15581  issrngd  15642  islmodd  15649  lmodscaf  15665  lmodvsghm  15702  lssacs  15740  idlmhm  15814  invlmhm  15815  lmhmvsca  15818  reslmhm2  15826  reslmhm2b  15827  pwsdiaglmhm  15830  issubrngd2  15959  divsrhm  16005  crngridl  16006  divscrng  16008  isnzr2  16031  domnmuln0  16055  opprdomn  16058  asclghm  16094  asclrhm  16097  psraddcl  16144  psrvscacl  16154  psrass23  16170  psrbagev1  16263  coe1sclmulfv  16375  expmhm  16465  zntoslem  16526  znfld  16530  phlipf  16572  tgclb  16724  topbas  16726  ntrss  16808  mretopd  16845  neissex  16880  cnpnei  17009  lmcnp  17048  ordthaus  17128  llynlly  17219  restnlly  17224  llyidm  17230  nllyidm  17231  ptbasin  17288  txcnp  17330  ist0-4  17436  kqt0lem  17443  isr0  17444  regr1lem2  17447  cmphmph  17495  conhmph  17496  fbun  17551  trfbas2  17554  isfil2  17567  isfild  17569  infil  17574  fbasfip  17579  fbasrn  17595  trfil2  17598  rnelfmlem  17663  fmfnfmlem3  17667  flimopn  17686  txflf  17717  fclsnei  17730  fclsfnflim  17738  fcfnei  17746  clssubg  17807  tgphaus  17815  divstgplem  17819  tsmsadd  17845  isxmet2d  17908  xmetlecl  17927  xmettpos  17929  imasdsf1olem  17953  imasf1oxmet  17955  imasf1omet  17956  elbl3  17967  metss  18070  comet  18075  stdbdxmet  18077  stdbdmet  18078  methaus  18082  nrmmetd  18113  abvmet  18114  isngp4  18149  subgngp  18167  nmoi2  18255  nmoleub  18256  nmoid  18267  bl2ioo  18314  zcld  18335  divcn  18388  divccn  18393  cncffvrn  18418  divccncf  18426  icoopnst  18453  clmzlmvsca  18610  cph2ass  18664  tchcph  18683  cfilfcls  18716  bcthlem2  18763  cldcss  18821  dvrec  19320  dvmptfsum  19338  aalioulem3  19730  taylply2  19763  dchrelbasd  20494  dchrmulcl  20504  pntrmax  20729  padicabv  20795  grpoidinvlem2  20888  grpoidinvlem3  20889  grponpncan  20938  ablo4  20970  ablomuldiv  20972  gxdi  20979  ghgrp  21051  ghsubgolem  21053  efghgrp  21056  nvaddsub4  21235  nvmeq0  21238  nvelbl  21278  nvelbl2  21279  sspmval  21325  sspival  21330  sspimsval  21332  lnosub  21353  dipsubdir  21442  sspph  21449  hvadd4  21631  hvpncan  21634  his35  21683  hiassdi  21686  shscli  21912  shmodsi  21984  chj4  22130  spansnmul  22159  spansncol  22163  spanunsni  22174  hoadd4  22380  hosubadd4  22410  lnopl  22510  unopf1o  22512  counop  22517  lnfnl  22527  hmopadj2  22537  eighmre  22559  lnopmi  22596  lnophsi  22597  hmops  22616  hmopm  22617  cnlnadjlem2  22664  adjmul  22688  adjadd  22689  kbass6  22717  mdslj1i  22915  mdslj2i  22916  mdslmd1lem1  22921  mdslmd2i  22926  chirredlem3  22988  xdivmul  23124  isoun  23257  ismeas  23545  cnpcon  23776  cvmseu  23822  ghomf1olem  24016  subdivcomb1  24105  axsegconlem1  24617  axlowdimlem15  24656  itg2addnclem2  25004  toplat  25393  clfsebs  25450  fprodadd  25455  isppm  25457  fprodneg  25481  fprodsub  25482  mulinvsca  25583  cnvtr  25719  distmlva  25791  distsava  25792  fneint  26380  fnessref  26396  tailfb  26429  fipreimaOLD  26518  fzadd2  26547  metf1o  26572  isbnd3b  26612  equivbnd  26617  heiborlem3  26640  rrnmet  26656  rrndstprj1  26657  rrntotbnd  26663  exidcl  26669  ghomco  26676  ghomdiv  26677  grpokerinj  26678  rngoneglmul  26685  rngonegrmul  26686  rngosubdi  26687  rngosubdir  26688  isdrngo2  26692  rngohomco  26708  rngoisocnv  26715  riscer  26722  crngm4  26731  crngohomfo  26734  idlsubcl  26751  inidl  26758  keridl  26760  ispridlc  26798  pridlc3  26801  dmncan1  26804  lcomf  26870  ismrc  26879  isnacs3  26888  mzpindd  26927  pellex  27023  monotoddzzfi  27130  lermxnn0  27140  rmyeq0  27143  rmyeq  27144  lermy  27145  jm2.27  27204  lsmfgcl  27275  pwssplit2  27292  pwssplit3  27293  frlmup1  27353  fsumcnsrcl  27474  rngunsnply  27481  psgnghm  27540  mndvcl  27549  mamulid  27561  isdomn3  27626  ofdivrec  27646  ofdivcan4  27647  fmulcl  27814  3cyclfrgrarn  28436  chordthmALT  29026  bnj563  29088  lflvscl  29889  3dim0  30268  linepsubN  30563  cdlemg2fvlem  31405  trlcoat  31534  istendod  31573  dva1dim  31796  dvhvaddcomN  31908  dihf11  32079  dihlatat  32149
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator