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

Theorem 3expa 1196
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 1195 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 432 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  3anidm23  1287  mp3an2  1312  mpd3an3  1325  rgen3  2890  moi2  3284  sbc3ie  3409  2if2  3987  preq12bg  4205  prel12g  4206  reuhypd  4674  otsndisj  4752  fvtp1g  6110  f1imass  6159  weisoeq  6238  f1ofveu  6278  f1ocnvfv3  6279  curry1f  6877  curry2f  6879  funsssuppss  6926  tfrlem11  7057  oalimcl  7209  oeordsuc  7243  oelim2  7244  nneob  7301  mapxpen  7683  findcard  7758  wemaplem3  7972  en2eqpr  8384  infxpabs  8591  infxp  8594  cfflb  8638  cfsmolem  8649  isf32lem12  8743  fin1a2lem9  8787  fin1a2s  8793  axcc3  8817  axdc3lem4  8832  zornn0g  8884  pwfseqlem4  9039  tskwun  9161  tskint  9162  tskxp  9164  tskmap  9165  gruf  9188  gruwun  9190  grutsk1  9198  addcanpi  9276  ltapi  9280  mul4  9747  add4  9794  2addsub  9833  addsubeq4  9834  muladd  9988  ltleadd  10034  receu  10193  p1le  10384  lemul12b  10398  lbinfm  10495  zdiv  10930  fzind  10958  fnn0ind  10959  uzss  11101  zbtwnre  11179  qmulcl  11199  qreccl  11201  xrlttr  11345  xaddass  11440  xmulasslem3  11477  xmulass  11478  xadddilem  11485  xrsupsslem  11497  xrinfmsslem  11498  supxrunb1  11510  ixxin  11545  ioo0  11553  ico0  11574  ioc0  11575  icc0  11576  iooshf  11602  prunioo  11648  ioojoin  11650  elfz5  11679  elfz0fzfz0  11776  elfzonelfzo  11879  fzind2  11891  mulexpz  12173  expsub  12180  digit2  12266  digit1  12267  facndiv  12333  faclbnd4lem4  12341  faclbnd4  12342  faclbnd5  12343  bccmpl  12354  bcval5  12363  bcpasc  12366  hashunx  12421  swrdspsleq  12635  swrdccat1  12644  swrdccat2  12645  swrdswrd  12647  cats1un  12663  crim  12910  absmax  13124  ello12r  13302  elo12r  13313  climshftlem  13359  2sumeq2dv  13489  expcnv  13637  rpnnen2lem7  13814  dvdsval3  13850  dvdsnegb  13861  muldvds1  13868  muldvds2  13869  dvdscmul  13870  dvdsmulc  13871  dvdsmulcr  13873  dvds2ln  13874  divalgb  13920  ndvdssub  13923  gcddiv  14045  rpexp1i  14120  phiprmpw  14164  pythagtriplem1  14198  pockthg  14282  infpnlem1  14286  4sqlem3  14326  0ramcl  14399  firest  14687  imasaddfnlem  14782  imasleval  14795  xpsfrn2  14824  mrerintcl  14851  iscatd  14927  clatleglb  15612  mreclatBAD  15673  pslem  15692  mrcmndind  15813  grplmulf1o  15919  grplactcnv  15945  mulgnn0subcl  15962  mulgsubcl  15963  mulgdir  15974  issubg2  16018  issubgrpd2  16019  cycsubgcl  16029  cycsubgss  16030  nmzsubg  16044  eqgen  16056  ghmmulg  16081  conjghm  16099  symgfixfo  16267  odeq  16377  odval2  16378  odf1  16387  dfod2  16389  gexdvds  16407  gexdvds2  16408  gexcl2  16412  gexdvds3  16413  sylow2blem2  16444  efgsp1  16558  efgrelexlemb  16571  mulgmhm  16639  mulgghm  16640  iscyggen2  16684  iscyg3  16689  srglmhm  16983  srgrmhm  16984  rnglghm  17046  rngrghm  17047  gsumdixpOLD  17053  gsumdixp  17054  dvdsrcl2  17095  crngunit  17107  kerf1hrm  17187  subrgugrp  17243  cntzsubr  17256  lmodvsdir  17331  lmodvsass  17332  lmodvsghm  17366  lsssubg  17398  lss1d  17404  islbs2  17595  lidlsubg  17657  divscrng  17682  lpigen  17698  xrsdsreval  18247  expghm  18312  expghmOLD  18313  mulgghm2  18314  mulgghm2OLD  18317  ip0r  18455  obs2ss  18543  islindf3  18644  scmatscm  18798  scmataddcl  18801  scmatsubcl  18802  scmatfo  18815  matunit  18963  cpmatelimp  18996  cpmatelimp2  18998  cpmatinvcl  19001  cpmatmcl  19003  mat2pmatf  19012  m2cpmf  19026  cpm2mf  19036  m2cpmfo  19040  m2cpminv  19044  decpmataa0  19052  pm2mpf  19082  pm2mpf1  19083  idpm2idmp  19085  pm2mpfo  19098  elcls2  19357  opnnei  19403  innei  19408  iscnp4  19546  cnpnei  19547  iscncl  19552  cnnei  19565  cnconst  19567  ordthauslem  19666  bwth  19692  1stccnp  19745  llyrest  19768  nllyrest  19769  kgenss  19795  xkoccn  19871  kqsat  19983  kqt0lem  19988  isr0  19989  fbssfi  20089  isfild  20110  filcon  20135  trfilss  20141  fgtr  20142  ufileu  20171  ufilen  20182  fmfnfmlem4  20209  fmfnfm  20210  hausflimi  20232  cnpflf2  20252  cnpflf  20253  cnflf  20254  cnpfcf  20293  cnfcf  20294  cnextcn  20318  tmdmulg  20342  clsnsg  20359  tsmsxplem1  20406  tsmsxp  20408  trust  20483  ustuqtop0  20494  ismeti  20579  isxmet2d  20581  elbl2ps  20643  elbl2  20644  xblpnfps  20649  xblpnf  20650  xbln0  20668  blin  20675  blssexps  20680  blssex  20681  blsscls2  20758  blcls  20760  blsscls  20761  metss  20762  metrest  20778  metcn  20797  metustblOLD  20834  metustbl  20835  metutopOLD  20836  psmetutop  20837  nmf2  20864  nmdvr  20930  nmoi  20986  nmoix  20987  nmoleub  20989  nghmcn  21003  xrsxmet  21065  iccntr  21077  metdsle  21107  icoopnst  21190  iocopnst  21191  icccvx  21201  pi1xfr  21306  lmmbr  21448  lmmbr2  21449  iscfil3  21463  iscau2  21467  cfilres  21486  bcthlem1  21514  bcthlem4  21517  bcthlem5  21518  rrxmet  21586  ioombl  21726  iccvolcl  21728  ioovolcl  21730  mbfi1fseqlem3  21875  mbfi1fseqlem4  21876  mbfi1fseqlem5  21877  ig1pcl  22327  ig1prsp  22329  aannenlem1  22474  taylplem1  22508  dvtaylp  22515  relogeftb  22713  logdivlt  22750  cxpexp  22793  rpcxpcl  22801  isppw2  23133  vmappw  23134  lgslem4  23318  lgscllem  23322  lgsneg1  23339  lgsne0  23352  brbtwn2  23900  ax5seglem1  23923  ax5seglem2  23924  axcontlem4  23962  nbgraf1olem5  24137  constr3cycl  24353  wwlknimp  24379  usg2wlkeq  24400  wwlknred  24415  wwlknext  24416  clwwlknprop  24464  3cyclfrgrarn1  24704  3cyclfrgrarn  24705  4cycl2vnunb  24709  frgrancvvdeqlemB  24731  usgreghash2spotv  24759  2spotmdisj  24761  grpoidinvlem3  24900  isvci  25167  nmcvcn  25297  ipval2lem2  25306  ipval2lem5  25312  sspival  25343  sspimsval  25345  isblo2  25390  nmoo0  25398  blocni  25412  isph  25429  sspph  25462  hvadd4  25645  hiassdi  25700  ocsh  25893  chj4  26145  spansncol  26178  pjjsi  26310  hoscl  26356  hodcl  26358  hoadd4  26395  homco1  26412  homulass  26413  hoadddi  26414  hoadddir  26415  unoplin  26531  adjvalval  26548  hmoplin  26553  bralnfn  26559  brafnmul  26562  lnopmi  26611  lnopcoi  26614  hmops  26631  hmopm  26632  nmophmi  26642  lnfncnbd  26668  cnlnadjlem2  26679  adjlnop  26697  adjmul  26703  adjadd  26704  branmfn  26716  kbass5  26731  kbass6  26732  leop2  26735  leopadd  26743  leopmuli  26744  pjimai  26787  atcvatlem  26996  chirredlem2  27002  mdsymlem3  27016  mdsymlem5  27018  sumdmdii  27026  sumdmdlem  27029  cdj3lem2a  27047  cdj3lem2b  27048  cdj3lem3a  27050  cdj3i  27052  xreceu  27302  toslublem  27333  tosglblem  27335  xrstos  27345  ogrpaddltbi  27387  archiabllem1a  27413  archiabllem1b  27414  archiabllem2c  27417  archiabl  27420  slmdvsdir  27437  slmdvsass  27438  ordtconlem1  27558  hasheuni  27747  ballotlemirc  28126  signspval  28165  txpcon  28333  cvmscld  28374  2cprodeq2dv  28650  dfrdg2  28821  wsuclem  28974  nobndlem8  29052  segconeu  29254  linecom  29393  linethru  29396  lineintmo  29400  heicant  29642  mblfinlem1  29644  mblfinlem3  29646  ismblfin  29648  cnambfre  29656  itg2addnclem2  29660  ftc1anclem1  29683  ftc1anclem5  29687  ftc1anclem6  29688  ftc2nc  29692  areacirclem2  29701  areacirclem4  29703  areacirclem5  29704  areacirc  29705  fnemeet2  29804  fnejoin2  29806  fzmul  29852  subspopn  29864  isbndx  29897  isbnd2  29898  isbnd3  29899  ssbnd  29903  prdstotbnd  29909  heibor1  29925  rrnmet  29944  rngonegmn1l  29971  rngohomco  29996  rngoisocnv  30003  rngoisoco  30004  crngohomfo  30022  isidlc  30031  rngoidl  30040  prnc  30083  ispridlc  30086  oddcomabszz  30500  acongtr  30536  rpnnen3lem  30593  islssfg  30636  lmhmfgsplit  30652  unxpwdom3  30661  hbtlem7  30694  sdrgacs  30771  hashgcdeq  30779  iocmbl  30801  nzss  30838  dvconstbi  30855  iccdifprioo  31136  fourierdlem74  31497  fourierdlem75  31498  ralxfrd2  31786  el2fzo  31822  usgra2pthlem1  31836  lcoss  32127  snlindsntorlem  32161  bnj1204  33156  cvrval2  34080  glbconxN  34183  hlrelat5N  34206  cvratlem  34226  cvrat2  34234  athgt  34261  3dim2  34273  llnn0  34321  lplnn0N  34352  lvoln0N  34396  snatpsubN  34555  paddasslem18  34642  pmod1i  34653  lhpexle2  34815  lhpexle3lem  34816  lhpexle3  34817  ldilcnv  34920  trlcnv  34970  trlnidatb  34982  cdleme32snaw  35240  cdleme32fvaw  35244  cdleme42ke  35290  cdlemeg46gf  35338  cdleme50trn12  35357  cdlemg1cex  35393  cdlemb3  35411  tgrpgrplem  35554  tgrpabl  35556  tendoplcl2  35583  tendo0pl  35596  tendoicl  35601  tendoipl  35602  cdlemkid3N  35738  tendoex  35780  erngdvlem4  35796  erngdvlem4-rN  35804  dib1dim  35971  dib1dim2  35974  dihglbcpreN  36106  dihmeetALTN  36133  dih1dimatlem  36135  dihatlat  36140
  Copyright terms: Public domain W3C validator