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  5070  fnfco  5407  mpt2eq3dva  5912  fovrnda  5991  grprinvd  6059  oaass  6559  omlimcl  6576  odi  6577  nnmsucr  6623  eroprf  6756  cflim2  7889  mulcanenq  8584  mul4  8981  add4  9027  2addsub  9065  addsubeq4  9066  subadd4  9091  muladd  9212  ltleadd  9257  divmul  9427  divne0  9436  div23  9443  div12  9446  divsubdir  9456  divcan5  9462  divmuleq  9465  divcan6  9467  divdiv32  9468  div2sub  9585  letrp1  9598  lemul12b  9613  lediv1  9621  lt2mul2div  9632  lemuldiv  9635  ltdiv2  9641  ledivdiv  9645  lediv2  9646  ltdiv23  9647  lediv23  9648  sup2  9710  cju  9742  nndivre  9781  nndivtr  9787  nn0addge1  10010  nn0addge2  10011  peano2uz2  10099  uzind  10103  uzind3  10105  fzind  10110  fnn0ind  10111  uzind4  10276  qre  10321  irrmul  10341  rpdivcl  10376  rerpdivcl  10381  xrinfmsslem  10626  ixxin  10673  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzaddel  10826  fzrev  10846  modlt  10981  modcyc  10999  axdc4uzlem  11044  expdiv  11152  swrd00  11451  swrdcl  11452  2shfti  11575  isermulc2  12131  fsummulc2  12246  dvdscmulr  12557  dvdsmulcr  12558  dvds2add  12560  dvds2sub  12561  dvdstr  12562  alzdvds  12578  divalg2  12604  dvdslegcd  12695  isprm6  12788  pcqcl  12909  vdwmc2  13026  ressinbas  13204  isposd  14089  pleval2i  14098  tosso  14142  clatl  14220  poslubmo  14250  mndplusf  14383  mndfo  14397  imasmnd2  14409  issubm2  14426  0mhm  14435  resmhm  14436  resmhm2  14437  resmhm2b  14438  mhmco  14439  mhmima  14440  submacs  14442  prdspjmhm  14443  pwsdiagmhm  14445  pwsco1mhm  14446  pwsco2mhm  14447  gsumwsubmcl  14461  gsumccat  14464  gsumwmhm  14467  grpinvcnv  14536  grpinvnzcl  14540  grpsubf  14545  mulgnnsubcl  14579  mulgnndir  14589  imasgrp2  14610  divsgrp2  14613  issubg4  14638  isnsg3  14651  nsgacs  14653  nsgid  14663  divsadd  14674  ghmmhm  14693  ghmmhmb  14694  idghm  14698  resghm  14699  ghmf1  14711  divsghm  14719  gaid  14753  subgga  14754  gass  14755  gasubg  14756  invoppggim  14833  lsmidm  14973  pj1ghm  15012  mulgnn0di  15125  mulgmhm  15127  mulgghm  15128  invghm  15130  ghmplusg  15138  ablnsg  15139  divsabl  15157  gsumval3eu  15190  gsumval3  15191  gsumzcl  15195  gsumzaddlem  15203  gsumzadd  15204  gsumzmhm  15210  gsumzoppg  15216  rnglghm  15388  rngrghm  15389  issubrg2  15565  issrngd  15626  islmodd  15633  lmodscaf  15649  lmodvsghm  15686  lssacs  15724  idlmhm  15798  invlmhm  15799  lmhmvsca  15802  reslmhm2  15810  reslmhm2b  15811  pwsdiaglmhm  15814  issubrngd2  15943  divsrhm  15989  crngridl  15990  divscrng  15992  isnzr2  16015  domnmuln0  16039  opprdomn  16042  asclghm  16078  asclrhm  16081  psraddcl  16128  psrvscacl  16138  psrass23  16154  psrbagev1  16247  coe1sclmulfv  16359  expmhm  16449  zntoslem  16510  znfld  16514  phlipf  16556  tgclb  16708  topbas  16710  ntrss  16792  mretopd  16829  neissex  16864  cnpnei  16993  lmcnp  17032  ordthaus  17112  llynlly  17203  restnlly  17208  llyidm  17214  nllyidm  17215  ptbasin  17272  txcnp  17314  ist0-4  17420  kqt0lem  17427  isr0  17428  regr1lem2  17431  cmphmph  17479  conhmph  17480  fbun  17535  trfbas2  17538  isfil2  17551  isfild  17553  infil  17558  fbasfip  17563  fbasrn  17579  trfil2  17582  rnelfmlem  17647  fmfnfmlem3  17651  flimopn  17670  txflf  17701  fclsnei  17714  fclsfnflim  17722  fcfnei  17730  clssubg  17791  tgphaus  17799  divstgplem  17803  tsmsadd  17829  isxmet2d  17892  xmetlecl  17911  xmettpos  17913  imasdsf1olem  17937  imasf1oxmet  17939  imasf1omet  17940  elbl3  17951  metss  18054  comet  18059  stdbdxmet  18061  stdbdmet  18062  methaus  18066  nrmmetd  18097  abvmet  18098  isngp4  18133  subgngp  18151  nmoi2  18239  nmoleub  18240  nmoid  18251  bl2ioo  18298  zcld  18319  divcn  18372  divccn  18377  cncffvrn  18402  divccncf  18410  icoopnst  18437  clmzlmvsca  18594  cph2ass  18648  tchcph  18667  cfilfcls  18700  bcthlem2  18747  cldcss  18805  dvrec  19304  dvmptfsum  19322  aalioulem3  19714  taylply2  19747  dchrelbasd  20478  dchrmulcl  20488  pntrmax  20713  padicabv  20779  grpoidinvlem2  20872  grpoidinvlem3  20873  grponpncan  20922  ablo4  20954  ablomuldiv  20956  gxdi  20963  ghgrp  21035  ghsubgolem  21037  efghgrp  21040  nvaddsub4  21219  nvmeq0  21222  nvelbl  21262  nvelbl2  21263  sspmval  21309  sspival  21314  sspimsval  21316  lnosub  21337  dipsubdir  21426  sspph  21433  hvadd4  21615  hvpncan  21618  his35  21667  hiassdi  21670  shscli  21896  shmodsi  21968  chj4  22114  spansnmul  22143  spansncol  22147  spanunsni  22158  hoadd4  22364  hosubadd4  22394  lnopl  22494  unopf1o  22496  counop  22501  lnfnl  22511  hmopadj2  22521  eighmre  22543  lnopmi  22580  lnophsi  22581  hmops  22600  hmopm  22601  cnlnadjlem2  22648  adjmul  22672  adjadd  22673  kbass6  22701  mdslj1i  22899  mdslj2i  22900  mdslmd1lem1  22905  mdslmd2i  22910  chirredlem3  22972  xdivmul  23108  isoun  23242  ismeas  23530  cnpcon  23761  cvmseu  23807  ghomf1olem  24001  subdivcomb1  24090  axsegconlem1  24545  axlowdimlem15  24584  toplat  25290  clfsebs  25347  fprodadd  25352  isppm  25354  fprodneg  25378  fprodsub  25379  mulinvsca  25480  cnvtr  25616  distmlva  25688  distsava  25689  fneint  26277  fnessref  26293  tailfb  26326  fipreimaOLD  26415  fzadd2  26444  metf1o  26469  isbnd3b  26509  equivbnd  26514  heiborlem3  26537  rrnmet  26553  rrndstprj1  26554  rrntotbnd  26560  exidcl  26566  ghomco  26573  ghomdiv  26574  grpokerinj  26575  rngoneglmul  26582  rngonegrmul  26583  rngosubdi  26584  rngosubdir  26585  isdrngo2  26589  rngohomco  26605  rngoisocnv  26612  riscer  26619  crngm4  26628  crngohomfo  26631  idlsubcl  26648  inidl  26655  keridl  26657  ispridlc  26695  pridlc3  26698  dmncan1  26701  lcomf  26767  ismrc  26776  isnacs3  26785  mzpindd  26824  pellex  26920  monotoddzzfi  27027  lermxnn0  27037  rmyeq0  27040  rmyeq  27041  lermy  27042  jm2.27  27101  lsmfgcl  27172  pwssplit2  27189  pwssplit3  27190  frlmup1  27250  fsumcnsrcl  27371  rngunsnply  27378  psgnghm  27437  mndvcl  27446  mamulid  27458  isdomn3  27523  ofdivrec  27543  ofdivcan4  27544  fmulcl  27711  chordthmALT  28710  bnj563  28772  lflvscl  29267  3dim0  29646  linepsubN  29941  cdlemg2fvlem  30783  trlcoat  30912  istendod  30951  dva1dim  31174  dvhvaddcomN  31286  dihf11  31457  dihlatat  31527
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