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

Theorem 3expa 1205
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 1204 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 433 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  3anidm23  1323  mp3an2  1348  mpd3an3  1361  rgen3  2858  moi2  3258  sbc3ie  3375  2if2  3963  preq12bg  4182  prel12g  4183  reuhypd  4649  otsndisj  4726  fvtp1g  6129  f1imass  6180  weisoeq  6261  f1ofveu  6300  f1ocnvfv3  6301  curry1f  6901  curry2f  6903  funsssuppss  6952  tfrlem11  7114  oalimcl  7269  oeordsuc  7303  oelim2  7304  nneob  7361  mapxpen  7744  findcard  7816  wemaplem3  8063  en2eqpr  8437  infxpabs  8640  infxp  8643  cfflb  8687  cfsmolem  8698  isf32lem12  8792  fin1a2lem9  8836  fin1a2s  8842  axcc3  8866  axdc3lem4  8881  zornn0g  8933  pwfseqlem4  9086  tskwun  9208  tskint  9209  tskxp  9211  tskmap  9212  gruf  9235  gruwun  9237  grutsk1  9245  addcanpi  9323  ltapi  9327  mul4  9801  add4  9848  2addsub  9888  addsubeq4  9889  muladd  10050  ltleadd  10096  receu  10256  p1le  10447  lemul12b  10461  lbinf  10559  lbinfmOLD  10560  zdiv  11006  fzind  11033  fnn0ind  11034  uzss  11179  zbtwnre  11262  qmulcl  11282  qreccl  11284  xrlttr  11439  xaddass  11535  xmulasslem3  11572  xmulass  11573  xadddilem  11580  xrsupsslem  11592  xrinfmsslem  11593  supxrunb1  11605  ixxin  11652  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  iooshf  11713  prunioo  11759  ioojoin  11761  elfz5  11790  elfz0fzfz0  11893  elfzonelfzo  12008  fzind2  12020  mulexpz  12309  expsub  12317  digit2  12402  digit1  12403  facndiv  12470  faclbnd4lem4  12478  faclbnd4  12479  faclbnd5  12480  bccmpl  12491  bcval5  12500  bcpasc  12503  hashunx  12562  ccatrn  12720  swrdccat1  12798  swrdccat2  12799  swrdswrd  12801  cats1un  12817  crim  13157  absmax  13371  ello12r  13559  elo12r  13570  climshftlem  13616  2sumeq2dv  13749  expcnv  13900  2cprodeq2dv  13957  rpnnen2lem7  14251  dvdsval3  14287  dvdsnegb  14298  muldvds1  14305  muldvds2  14306  dvdscmul  14307  dvdsmulc  14308  dvdsmulcr  14310  dvds2ln  14311  divalgb  14360  ndvdssub  14363  gcddiv  14488  lcmfval  14562  lcmfvalOLD  14566  lcmfcl  14572  dvdslcmf  14575  rpexp1i  14644  phiprmpw  14693  pythagtriplem1  14729  pockthg  14813  infpnlem1  14817  4sqlem3  14857  0ramcl  14944  firest  15290  imasaddfnlem  15385  imasleval  15398  xpsfrn2  15427  mrerintcl  15454  iscatd  15530  fullestrcsetc  15987  fullsetcestrc  16002  clatleglb  16323  mreclatBAD  16384  pslem  16403  mrcmndind  16564  grplmulf1o  16679  grplactcnv  16705  mulgnn0subcl  16722  mulgsubcl  16723  mulgdir  16734  issubg2  16783  issubgrpd2  16784  cycsubgcl  16794  cycsubgss  16795  nmzsubg  16809  eqgen  16821  ghmmulg  16846  conjghm  16864  symgfixfo  17031  odeq  17141  odval2  17142  odf1  17151  dfod2  17153  gexdvds  17171  gexdvds2  17172  gexcl2  17176  gexdvds3  17177  sylow2blem2  17208  efgsp1  17322  efgrelexlemb  17335  mulgmhm  17403  mulgghm  17404  iscyggen2  17451  iscyg3  17456  srglmhm  17703  srgrmhm  17704  ringlghm  17767  ringrghm  17768  gsumdixp  17772  dvdsrcl2  17813  crngunit  17825  kerf1hrm  17906  subrgugrp  17962  cntzsubr  17975  lmodvsdir  18050  lmodvsass  18051  lmodvsghm  18084  lsssubg  18115  lss1d  18121  islbs2  18312  lidlsubg  18373  lidlsubcl  18374  quscrng  18399  lpigen  18415  xrsdsreval  18948  expghm  18998  mulgghm2  18999  ip0r  19135  obs2ss  19223  islindf3  19315  scmatscm  19469  scmataddcl  19472  scmatsubcl  19473  scmatfo  19486  matunit  19634  cpmatelimp  19667  cpmatelimp2  19669  cpmatinvcl  19672  cpmatmcl  19674  mat2pmatf  19683  m2cpmf  19697  cpm2mf  19707  m2cpmfo  19711  m2cpminv  19715  decpmataa0  19723  pm2mpf  19753  pm2mpf1  19754  idpm2idmp  19756  pm2mpfo  19769  elcls2  20021  opnnei  20067  innei  20072  iscnp4  20210  cnpnei  20211  iscncl  20216  cnnei  20229  cnconst  20231  ordthauslem  20330  bwth  20356  1stccnp  20408  llyrest  20431  nllyrest  20432  kgenss  20489  xkoccn  20565  kqsat  20677  kqt0lem  20682  isr0  20683  fbssfi  20783  isfild  20804  filcon  20829  trfilss  20835  fgtr  20836  ufileu  20865  ufilen  20876  fmfnfmlem4  20903  fmfnfm  20904  hausflimi  20926  cnpflf2  20946  cnpflf  20947  cnflf  20948  cnpfcf  20987  cnfcf  20988  cnextcn  21013  tmdmulg  21038  clsnsg  21055  tsmsxplem1  21098  tsmsxp  21100  trust  21175  ustuqtop0  21186  ismeti  21271  isxmet2d  21273  elbl2ps  21335  elbl2  21336  xblpnfps  21341  xblpnf  21342  xbln0  21360  blin  21367  blssexps  21372  blssex  21373  blsscls2  21450  blcls  21452  blsscls  21453  metss  21454  metrest  21470  metcn  21489  metustbl  21512  psmetutop  21513  nmf2  21538  nmdvr  21604  nmoi  21660  nmoix  21661  nmoleub  21663  nghmcn  21677  xrsxmet  21738  iccntr  21750  metdsle  21780  icoopnst  21863  iocopnst  21864  icccvx  21874  pi1xfr  21979  lmmbr  22121  lmmbr2  22122  iscfil3  22136  iscau2  22140  cfilres  22159  bcthlem1  22185  bcthlem4  22188  bcthlem5  22189  rrxmet  22255  ioombl  22395  iccvolcl  22397  ioovolcl  22399  mbfi1fseqlem3  22552  mbfi1fseqlem4  22553  mbfi1fseqlem5  22554  ig1pcl  23001  ig1prsp  23003  aannenlem1  23149  taylplem1  23183  dvtaylp  23190  relogeftb  23399  logdivlt  23435  cxpexp  23478  rpcxpcl  23486  isppw2  23905  vmappw  23906  lgslem4  24090  lgscllem  24094  lgsneg1  24111  lgsne0  24124  cgraswap  24718  brbtwn2  24781  ax5seglem1  24804  ax5seglem2  24805  axcontlem4  24843  nbgraf1olem5  25018  constr3cycl  25234  wwlknimp  25260  usg2wlkeq  25281  wwlknred  25296  wwlknext  25297  clwwlknprop  25345  3cyclfrgrarn1  25585  3cyclfrgrarn  25586  4cycl2vnunb  25590  frgrancvvdeqlemB  25611  usgreghash2spotv  25639  2spotmdisj  25641  grpoidinvlem3  25779  isvci  26046  nmcvcn  26176  ipval2lem2  26185  ipval2lem5  26191  sspival  26222  sspimsval  26224  isblo2  26269  nmoo0  26277  blocni  26291  isph  26308  sspph  26341  hvadd4  26524  hiassdi  26579  ocsh  26771  chj4  27023  spansncol  27056  pjjsi  27188  hoscl  27233  hodcl  27235  hoadd4  27272  homco1  27289  homulass  27290  hoadddi  27291  hoadddir  27292  unoplin  27408  adjvalval  27425  hmoplin  27430  bralnfn  27436  brafnmul  27439  lnopmi  27488  lnopcoi  27491  hmops  27508  hmopm  27509  nmophmi  27519  lnfncnbd  27545  cnlnadjlem2  27556  adjlnop  27574  adjmul  27580  adjadd  27581  branmfn  27593  kbass5  27608  kbass6  27609  leop2  27612  leopadd  27620  leopmuli  27621  pjimai  27664  atcvatlem  27873  chirredlem2  27879  mdsymlem3  27893  mdsymlem5  27895  sumdmdii  27903  sumdmdlem  27906  cdj3lem2a  27924  cdj3lem2b  27925  cdj3lem3a  27927  cdj3i  27929  xreceu  28229  toslublem  28266  tosglblem  28268  ogrpaddltbi  28320  archiabllem1b  28347  archiabllem2c  28350  archiabl  28353  slmdvsdir  28370  slmdvsass  28371  pstmxmet  28539  ordtconlem1  28569  hasheuni  28745  omsf  28957  ballotlemirc  29190  signswmnd  29234  bnj1204  29609  txpcon  29743  cvmscld  29784  elmpps  29999  dfrdg2  30229  wsuclem  30295  nobndlem8  30373  segconeu  30563  linecom  30702  linethru  30705  lineintmo  30709  fnemeet2  30808  fnejoin2  30810  heicant  31679  mblfinlem1  31681  mblfinlem3  31683  ismblfin  31685  cnambfre  31693  itg2addnclem2  31698  ftc1anclem1  31721  ftc1anclem5  31725  ftc1anclem6  31726  ftc2nc  31730  areacirclem2  31737  areacirclem4  31739  areacirclem5  31740  areacirc  31741  fzmul  31773  subspopn  31785  isbndx  31818  isbnd2  31819  isbnd3  31820  ssbnd  31824  prdstotbnd  31830  heibor1  31846  rrnmet  31865  rngonegmn1l  31892  rngohomco  31917  rngoisocnv  31924  rngoisoco  31925  crngohomfo  31943  isidlc  31952  rngoidl  31961  prnc  32004  ispridlc  32007  cvrval2  32549  glbconxN  32652  hlrelat5N  32675  cvratlem  32695  cvrat2  32703  athgt  32730  3dim2  32742  llnn0  32790  lplnn0N  32821  lvoln0N  32865  snatpsubN  33024  paddasslem18  33111  pmod1i  33122  lhpexle2  33284  lhpexle3lem  33285  lhpexle3  33286  ldilcnv  33389  trlcnv  33440  trlnidatb  33452  cdleme32snaw  33711  cdleme32fvaw  33715  cdleme42ke  33761  cdlemeg46gf  33809  cdleme50trn12  33828  cdlemg1cex  33864  cdlemb3  33882  tgrpgrplem  34025  tgrpabl  34027  tendoplcl2  34054  tendo0pl  34067  tendoicl  34072  tendoipl  34073  cdlemkid3N  34209  tendoex  34251  erngdvlem4  34267  erngdvlem4-rN  34275  dib1dim  34442  dib1dim2  34445  dihglbcpreN  34577  dihmeetALTN  34604  dih1dimatlem  34606  dihatlat  34611  oddcomabszz  35498  acongtr  35534  rpnnen3lem  35592  islssfg  35634  lmhmfgsplit  35650  unxpwdom3  35659  hbtlem7  35690  sdrgacs  35766  hashgcdeq  35774  iocmbl  35796  ss2iundf  35890  nzss  36303  dvconstbi  36320  bccbc  36331  uzmptshftfval  36332  iccdifprioo  37202  dvnmul  37387  fourierdlem74  37612  fourierdlem75  37613  sge0iunmptlemfi  37789  sge0iunmptlemre  37791  sge0iunmpt  37794  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  pfxccat1  38341  ralxfrd2  38380  usgra2pthlem1  38423  rnghmsubcsetclem2  38736  rhmsubcsetclem2  38782  rhmsubcrngclem2  38788  lcoss  38989  snlindsntorlem  39023  aacllem  39301
  Copyright terms: Public domain W3C validator