MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3expb 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  5220  fnfco  5568  mpt2eq3dva  6097  fovrnda  6176  grprinvd  6245  oaass  6763  omlimcl  6780  odi  6781  nnmsucr  6827  cflim2  8099  mulcanenq  8793  mul4  9191  add4  9237  2addsub  9275  addsubeq4  9276  subadd4  9301  muladd  9422  ltleadd  9467  divmul  9637  divne0  9646  div23  9653  div12  9656  divsubdir  9666  divcan5  9672  divmuleq  9675  divcan6  9677  divdiv32  9678  div2sub  9795  letrp1  9808  lemul12b  9823  lediv1  9831  lt2mul2div  9842  lemuldiv  9845  ltdiv2  9851  ledivdiv  9855  lediv2  9856  ltdiv23  9857  lediv23  9858  sup2  9920  cju  9952  nndivre  9991  nndivtr  9997  nn0addge1  10222  nn0addge2  10223  peano2uz2  10313  uzind  10317  uzind3  10319  fzind  10324  fnn0ind  10325  uzind4  10490  qre  10535  irrmul  10555  rpdivcl  10590  rerpdivcl  10595  xrinfmsslem  10842  ixxin  10889  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  fzaddel  11043  fzrev  11064  modlt  11213  modcyc  11231  axdc4uzlem  11276  expdiv  11385  swrd00  11720  swrdcl  11721  2shfti  11850  isermulc2  12406  fsummulc2  12522  dvdscmulr  12833  dvdsmulcr  12834  dvds2add  12836  dvds2sub  12837  dvdstr  12838  alzdvds  12854  divalg2  12880  dvdslegcd  12971  isprm6  13064  pcqcl  13185  vdwmc2  13302  ressinbas  13480  isposd  14367  pleval2i  14376  tosso  14420  clatl  14498  poslubmo  14528  mndplusf  14661  mndfo  14675  imasmnd2  14687  issubm2  14704  0mhm  14713  resmhm  14714  resmhm2  14715  resmhm2b  14716  mhmco  14717  mhmima  14718  submacs  14720  prdspjmhm  14721  pwsdiagmhm  14723  pwsco1mhm  14724  pwsco2mhm  14725  gsumwsubmcl  14739  gsumccat  14742  gsumwmhm  14745  grpinvcnv  14814  grpinvnzcl  14818  grpsubf  14823  mulgnnsubcl  14857  mulgnndir  14867  imasgrp2  14888  divsgrp2  14891  issubg4  14916  isnsg3  14929  nsgacs  14931  nsgid  14941  divsadd  14952  ghmmhm  14971  ghmmhmb  14972  idghm  14976  resghm  14977  ghmf1  14989  divsghm  14997  gaid  15031  subgga  15032  gasubg  15034  invoppggim  15111  lsmidm  15251  pj1ghm  15290  mulgnn0di  15403  mulgmhm  15405  mulgghm  15406  invghm  15408  ghmplusg  15416  ablnsg  15417  divsabl  15435  gsumval3eu  15468  gsumval3  15469  gsumzcl  15473  gsumzaddlem  15481  gsumzadd  15482  gsumzmhm  15488  gsumzoppg  15494  rnglghm  15666  rngrghm  15667  issubrg2  15843  issrngd  15904  islmodd  15911  lmodscaf  15927  lmodvsghm  15960  lssacs  15998  idlmhm  16072  invlmhm  16073  lmhmvsca  16076  reslmhm2  16084  reslmhm2b  16085  pwsdiaglmhm  16088  issubrngd2  16217  divsrhm  16263  crngridl  16264  divscrng  16266  isnzr2  16289  domnmuln0  16313  opprdomn  16316  asclghm  16352  asclrhm  16355  psraddcl  16402  psrvscacl  16412  psrass23  16428  psrbagev1  16521  coe1sclmulfv  16630  expmhm  16731  zntoslem  16792  znfld  16796  phlipf  16838  tgclb  16990  topbas  16992  ntrss  17074  mretopd  17111  neissex  17146  cnpnei  17282  lmcnp  17322  ordthaus  17402  llynlly  17493  restnlly  17498  llyidm  17504  nllyidm  17505  ptbasin  17562  txcnp  17605  ist0-4  17714  kqt0lem  17721  isr0  17722  regr1lem2  17725  cmphmph  17773  conhmph  17774  fbun  17825  trfbas2  17828  isfil2  17841  isfild  17843  infil  17848  fbasfip  17853  fbasrn  17869  trfil2  17872  rnelfmlem  17937  fmfnfmlem3  17941  flimopn  17960  txflf  17991  fclsnei  18004  fclsfnflim  18012  fcfnei  18020  clssubg  18091  tgphaus  18099  divstgplem  18103  tsmsadd  18129  psmetxrge0  18297  psmetlecl  18299  xmetlecl  18329  xmettpos  18332  imasdsf1olem  18356  imasf1oxmet  18358  imasf1omet  18359  elbl3ps  18374  elbl3  18375  metss  18491  comet  18496  stdbdxmet  18498  stdbdmet  18499  methaus  18503  nrmmetd  18575  abvmet  18576  isngp4  18611  subgngp  18629  nmoi2  18717  nmoleub  18718  nmoid  18729  bl2ioo  18776  zcld  18797  divcn  18851  divccn  18856  cncffvrn  18881  divccncf  18889  icoopnst  18917  clmzlmvsca  19074  cph2ass  19128  tchcph  19147  cfilfcls  19180  bcthlem2  19231  cldcss  19295  dvrec  19794  dvmptfsum  19812  aalioulem3  20204  taylply2  20237  dchrelbasd  20976  dchrmulcl  20986  pntrmax  21211  padicabv  21277  usgraidx2vlem1  21363  usgraidx2vlem2  21364  grpoidinvlem2  21746  grpoidinvlem3  21747  grponpncan  21796  ablo4  21828  ablomuldiv  21830  gxdi  21837  ghgrp  21909  ghsubgolem  21911  efghgrp  21914  nvaddsub4  22095  nvmeq0  22098  nvelbl  22138  nvelbl2  22139  sspmval  22185  sspival  22190  sspimsval  22192  lnosub  22213  dipsubdir  22302  sspph  22309  hvadd4  22491  hvpncan  22494  his35  22543  hiassdi  22546  shscli  22772  shmodsi  22844  chj4  22990  spansnmul  23019  spansncol  23023  spanunsni  23034  hoadd4  23240  hosubadd4  23270  lnopl  23370  unopf1o  23372  counop  23377  lnfnl  23387  hmopadj2  23397  eighmre  23419  lnopmi  23456  lnophsi  23457  hmops  23476  hmopm  23477  cnlnadjlem2  23524  adjmul  23548  adjadd  23549  kbass6  23577  mdslj1i  23775  mdslj2i  23776  mdslmd1lem1  23781  mdslmd2i  23786  chirredlem3  23848  isoun  24042  xdivmul  24124  isarchi2  24208  metider  24242  ismeas  24506  dya2iocnei  24585  cnpcon  24870  cvmseu  24916  ghomf1olem  25058  subdivcomb1  25148  axsegconlem1  25760  axlowdimlem15  25799  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  cnambfre  26154  itg2addnclem2  26156  fneint  26247  fnessref  26263  tailfb  26296  fzadd2  26335  metf1o  26351  isbnd3b  26384  equivbnd  26389  heiborlem3  26412  rrnmet  26428  rrndstprj1  26429  rrntotbnd  26435  exidcl  26441  ghomco  26448  ghomdiv  26449  grpokerinj  26450  rngoneglmul  26457  rngonegrmul  26458  rngosubdi  26459  rngosubdir  26460  isdrngo2  26464  rngohomco  26480  rngoisocnv  26487  riscer  26494  crngm4  26503  crngohomfo  26506  idlsubcl  26523  inidl  26530  keridl  26532  ispridlc  26570  pridlc3  26573  dmncan1  26576  lcomf  26636  ismrc  26645  isnacs3  26654  mzpindd  26693  pellex  26788  monotoddzzfi  26895  lermxnn0  26905  rmyeq0  26908  rmyeq  26909  lermy  26910  jm2.27  26969  lsmfgcl  27040  pwssplit2  27057  pwssplit3  27058  frlmup1  27118  fsumcnsrcl  27239  rngunsnply  27246  psgnghm  27305  mndvcl  27314  isdomn3  27391  ofdivrec  27411  ofdivcan4  27412  fmulcl  27578  swrdccatin12lem3  28024  3cyclfrgrarn  28117  frgrawopreg  28152  chordthmALT  28755  bnj563  28817  lflvscl  29560  3dim0  29939  linepsubN  30234  cdlemg2fvlem  31076  trlcoat  31205  istendod  31244  dva1dim  31467  dvhvaddcomN  31579  dihf11  31750  dihlatat  31820
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