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

Theorem 3expa 1153
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
3expa  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1152 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 422 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3anidm23  1243  mp3an2  1267  mpd3an3  1280  rgen3  2739  moi2  3051  sbc3ie  3166  preq12bg  3912  reuhypd  4683  fvtp1g  5874  f1imass  5942  fcof1o  5958  weisoeq  6008  curry1f  6372  curry2f  6374  riota5OLD  6505  f1ofveu  6513  f1ocnvfv3  6514  tfrlem11  6578  oalimcl  6732  oeordsuc  6766  oelim2  6767  nneob  6824  mapxpen  7202  findcard  7276  wemaplem3  7443  en2eqpr  7817  infxpabs  8018  infxp  8021  cfflb  8065  cfsmolem  8076  isf32lem12  8170  fin1a2lem9  8214  fin1a2s  8220  axcc3  8244  axdc3lem4  8259  zornn0g  8311  pwfseqlem4  8463  tskwun  8585  tskint  8586  tskxp  8588  tskmap  8589  gruf  8612  gruwun  8614  grutsk1  8622  addcanpi  8702  ltapi  8706  mul4  9160  add4  9206  2addsub  9244  addsubeq4  9245  muladd  9391  ltleadd  9436  receu  9592  p1le  9778  lemul12b  9792  lbinfm  9886  zdiv  10265  fzind  10293  fnn0ind  10294  uzss  10431  zbtwnre  10497  qmulcl  10517  qreccl  10519  xrlttr  10658  xaddass  10753  xmulasslem3  10790  xmulass  10791  xadddilem  10798  xrsupsslem  10810  xrinfmsslem  10811  supxrunb1  10823  ixxin  10858  ioo0  10866  ico0  10887  ioc0  10888  icc0  10889  iooshf  10914  prunioo  10950  ioojoin  10952  elfz5  10976  fzind2  11118  mulexpz  11340  expsub  11347  digit2  11432  digit1  11433  facndiv  11499  faclbnd4lem4  11507  faclbnd4  11508  faclbnd5  11509  bccmpl  11520  bcval5  11529  bcpasc  11532  hashunx  11580  swrdccat1  11694  swrdccat2  11695  cats1un  11710  crim  11840  absmax  12053  ello12r  12231  elo12r  12242  climshftlem  12288  2sumeq2dv  12419  expcnv  12563  rpnnen2lem7  12740  dvdsval3  12776  dvdsnegb  12787  muldvds1  12794  muldvds2  12795  dvdscmul  12796  dvdsmulc  12797  dvdsmulcr  12799  dvds2ln  12800  divalgb  12844  ndvdssub  12847  gcddiv  12969  rpexp1i  13041  phiprmpw  13085  pythagtriplem1  13110  pockthg  13194  infpnlem1  13198  4sqlem3  13238  0ramcl  13311  firest  13580  imasaddfnlem  13673  imasleval  13686  xpsfrn2  13715  mrerintcl  13742  iscatd  13818  lubid  14359  clatleglb  14473  mreclat  14533  pslem  14558  grplmulf1o  14785  grplactcnv  14807  mulgnn0subcl  14823  mulgsubcl  14824  mulgdir  14835  issubg2  14879  cycsubgcl  14886  cycsubgss  14887  nmzsubg  14901  eqgen  14913  ghmmulg  14938  conjghm  14956  odeq  15108  odval2  15109  odf1  15118  dfod2  15120  gexdvds  15138  gexdvds2  15139  gexcl2  15143  gexdvds3  15144  sylow2blem2  15175  efgsp1  15289  efgrelexlemb  15302  mulgmhm  15370  mulgghm  15371  iscyggen2  15411  iscyg3  15416  rnglghm  15631  rngrghm  15632  gsumdixp  15635  dvdsrcl2  15675  crngunit  15687  subrgugrp  15807  cntzsubr  15820  lmodvsdir  15894  lmodvsass  15895  lmodvsghm  15925  lsssubg  15953  lss1d  15959  islbs2  16146  issubgrpd2  16180  lidlsubg  16206  divscrng  16231  lpigen  16247  xrsdsreval  16659  expghm  16693  mulgghm2  16702  ip0r  16784  obs2ss  16872  elcls2  17054  opnnei  17100  innei  17105  iscnp4  17242  cnpnei  17243  iscncl  17248  cnnei  17261  cnconst  17263  ordthauslem  17362  1stccnp  17439  llyrest  17462  nllyrest  17463  kgenss  17489  xkoccn  17565  kqsat  17677  kqt0lem  17682  isr0  17683  fbssfi  17783  isfild  17804  filcon  17829  trfilss  17835  fgtr  17836  ufileu  17865  ufilen  17876  fmfnfmlem4  17903  fmfnfm  17904  hausflimi  17926  cnpflf2  17946  cnpflf  17947  cnflf  17948  cnpfcf  17987  cnfcf  17988  cnextcn  18012  tmdmulg  18036  clsnsg  18053  tsmsxplem1  18096  tsmsxp  18098  trust  18173  ustuqtop0  18184  ismeti  18257  isxmet2d  18259  elbl2  18317  xblpnf  18320  xbln0  18332  blin  18337  blssex  18340  blsscls2  18417  blcls  18419  blsscls  18420  metss  18421  metrest  18437  metcn  18456  metustbl  18479  metutop  18480  nmf2  18504  nmdvr  18570  nmoi  18626  nmoix  18627  nmoleub  18629  nghmcn  18643  xrsxmet  18704  iccntr  18716  metdsle  18746  icoopnst  18828  iocopnst  18829  icccvx  18839  pi1xfr  18944  lmmbr  19075  lmmbr2  19076  iscfil3  19090  iscau2  19094  cfilres  19113  bcthlem1  19139  bcthlem4  19142  bcthlem5  19143  ioombl  19319  iccvolcl  19321  mbfi1fseqlem3  19469  mbfi1fseqlem4  19470  mbfi1fseqlem5  19471  ig1pcl  19958  ig1prsp  19960  aannenlem1  20105  taylplem1  20139  dvtaylp  20146  relogeftb  20339  logdivlt  20376  cxpexp  20419  rpcxpcl  20427  isppw2  20758  vmappw  20759  lgslem4  20943  lgscllem  20947  lgsneg1  20964  lgsne0  20977  nbgraf1olem5  21314  constr3cycl  21489  grpoidinvlem3  21635  isvci  21902  nmcvcn  22032  ipval2lem2  22041  ipval2lem5  22047  sspival  22078  sspimsval  22080  isblo2  22125  nmoo0  22133  blocni  22147  isph  22164  sspph  22197  hvadd4  22379  hiassdi  22434  ocsh  22626  chj4  22878  spansncol  22911  pjjsi  23043  hoscl  23089  hodcl  23091  hoadd4  23128  homco1  23145  homulass  23146  hoadddi  23147  hoadddir  23148  unoplin  23264  adjvalval  23281  hmoplin  23286  bralnfn  23292  brafnmul  23295  lnopmi  23344  lnopcoi  23347  hmops  23364  hmopm  23365  nmophmi  23375  lnfncnbd  23401  cnlnadjlem2  23412  adjlnop  23430  adjmul  23436  adjadd  23437  branmfn  23449  kbass5  23464  kbass6  23465  leop2  23468  leopadd  23476  leopmuli  23477  pjimai  23520  atcvatlem  23729  chirredlem2  23735  mdsymlem3  23749  mdsymlem5  23751  sumdmdii  23759  sumdmdlem  23762  cdj3lem2a  23780  cdj3lem2b  23781  cdj3lem3a  23783  cdj3i  23785  xreceu  23999  hasheuni  24264  ballotlemirc  24561  txpcon  24691  cvmscld  24732  2cprodeq2dv  25023  dfrdg2  25169  nobndlem8  25370  brbtwn2  25551  ax5seglem1  25574  ax5seglem2  25575  axcontlem4  25613  segconeu  25652  linecom  25791  linethru  25794  lineintmo  25798  itg2addnclem2  25951  areacirclem4  25977  areacirclem5  25979  areacirclem6  25980  areacirc  25981  fnemeet2  26080  fnejoin2  26082  fzmul  26128  subspopn  26142  isbndx  26175  isbnd2  26176  isbnd3  26177  ssbnd  26181  prdstotbnd  26187  heibor1  26203  rrnmet  26222  rngonegmn1l  26249  rngohomco  26274  rngoisocnv  26281  rngoisoco  26282  crngohomfo  26300  isidlc  26309  rngoidl  26318  prnc  26361  ispridlc  26364  oddcomabszz  26691  acongtr  26727  rpnnen3lem  26786  islssfg  26830  lmhmfgsplit  26846  unxpwdom3  26918  islindf3  26958  hbtlem7  26991  sdrgacs  27171  hashgcdeq  27179  dvconstbi  27213  ioovolcl  27403  3cyclfrgrarn1  27758  3cyclfrgrarn  27759  4cycl2vnunb  27763  frgrancvvdeqlemB  27783  bnj1204  28712  cvrval2  29440  glbconxN  29543  hlrelat5N  29566  cvratlem  29586  cvrat2  29594  athgt  29621  3dim2  29633  llnn0  29681  lplnn0N  29712  lvoln0N  29756  snatpsubN  29915  paddasslem18  30002  pmod1i  30013  lhpexle2  30175  lhpexle3lem  30176  lhpexle3  30177  ldilcnv  30280  trlcnv  30330  trlnidatb  30342  cdleme32snaw  30600  cdleme32fvaw  30604  cdleme42ke  30650  cdlemeg46gf  30698  cdleme50trn12  30717  cdlemg1cex  30753  cdlemb3  30771  tgrpgrplem  30914  tgrpabl  30916  tendoplcl2  30943  tendo0pl  30956  tendoicl  30961  tendoipl  30962  cdlemkid3N  31098  tendoex  31140  erngdvlem4  31156  erngdvlem4-rN  31164  dib1dim  31331  dib1dim2  31334  dihglbcpreN  31466  dihmeetALTN  31493  dih1dimatlem  31495  dihatlat  31500
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