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

Theorem 3expa 1187
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 1186 . 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 965
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 967
This theorem is referenced by:  3anidm23  1277  mp3an2  1302  mpd3an3  1315  rgen3  2808  moi2  3135  sbc3ie  3259  2if2  3832  preq12bg  4046  prel12g  4047  reuhypd  4514  fvtp1g  5923  f1imass  5972  fcof1o  5992  weisoeq  6041  f1ofveu  6081  f1ocnvfv3  6082  curry1f  6661  curry2f  6663  funsssuppss  6710  tfrlem11  6839  oalimcl  6991  oeordsuc  7025  oelim2  7026  nneob  7083  mapxpen  7469  findcard  7543  wemaplem3  7754  en2eqpr  8166  infxpabs  8373  infxp  8376  cfflb  8420  cfsmolem  8431  isf32lem12  8525  fin1a2lem9  8569  fin1a2s  8575  axcc3  8599  axdc3lem4  8614  zornn0g  8666  pwfseqlem4  8821  tskwun  8943  tskint  8944  tskxp  8946  tskmap  8947  gruf  8970  gruwun  8972  grutsk1  8980  addcanpi  9060  ltapi  9064  mul4  9530  add4  9577  2addsub  9616  addsubeq4  9617  muladd  9769  ltleadd  9814  receu  9973  p1le  10164  lemul12b  10178  lbinfm  10275  zdiv  10704  fzind  10732  fnn0ind  10733  uzss  10873  zbtwnre  10943  qmulcl  10963  qreccl  10965  xrlttr  11109  xaddass  11204  xmulasslem3  11241  xmulass  11242  xadddilem  11249  xrsupsslem  11261  xrinfmsslem  11262  supxrunb1  11274  ixxin  11309  ioo0  11317  ico0  11338  ioc0  11339  icc0  11340  iooshf  11366  prunioo  11406  ioojoin  11408  elfz5  11437  elfz0fzfz0  11477  elfzonelfzo  11619  fzind2  11629  mulexpz  11896  expsub  11903  digit2  11989  digit1  11990  facndiv  12056  faclbnd4lem4  12064  faclbnd4  12065  faclbnd5  12066  bccmpl  12077  bcval5  12086  bcpasc  12089  hashunx  12141  swrdspsleq  12334  swrdccat1  12343  swrdccat2  12344  swrdswrd  12346  cats1un  12362  crim  12596  absmax  12809  ello12r  12987  elo12r  12998  climshftlem  13044  2sumeq2dv  13174  expcnv  13318  rpnnen2lem7  13495  dvdsval3  13531  dvdsnegb  13542  muldvds1  13549  muldvds2  13550  dvdscmul  13551  dvdsmulc  13552  dvdsmulcr  13554  dvds2ln  13555  divalgb  13600  ndvdssub  13603  gcddiv  13725  rpexp1i  13799  phiprmpw  13843  pythagtriplem1  13875  pockthg  13959  infpnlem1  13963  4sqlem3  14003  0ramcl  14076  firest  14363  imasaddfnlem  14458  imasleval  14471  xpsfrn2  14500  mrerintcl  14527  iscatd  14603  clatleglb  15288  mreclatBAD  15349  pslem  15368  mrcmndind  15485  grplmulf1o  15591  grplactcnv  15615  mulgnn0subcl  15631  mulgsubcl  15632  mulgdir  15643  issubg2  15687  issubgrpd2  15688  cycsubgcl  15698  cycsubgss  15699  nmzsubg  15713  eqgen  15725  ghmmulg  15750  conjghm  15768  symgfixfo  15936  odeq  16044  odval2  16045  odf1  16054  dfod2  16056  gexdvds  16074  gexdvds2  16075  gexcl2  16079  gexdvds3  16080  sylow2blem2  16111  efgsp1  16225  efgrelexlemb  16238  mulgmhm  16306  mulgghm  16307  iscyggen2  16349  iscyg3  16354  srglmhm  16622  srgrmhm  16623  rnglghm  16681  rngrghm  16682  gsumdixpOLD  16688  gsumdixp  16689  dvdsrcl2  16730  crngunit  16742  subrgugrp  16862  cntzsubr  16875  lmodvsdir  16950  lmodvsass  16951  lmodvsghm  16984  lsssubg  17015  lss1d  17021  islbs2  17212  lidlsubg  17274  divscrng  17299  lpigen  17315  xrsdsreval  17833  expghm  17898  expghmOLD  17899  mulgghm2  17900  mulgghm2OLD  17903  ip0r  18041  obs2ss  18129  islindf3  18230  matunit  18459  elcls2  18653  opnnei  18699  innei  18704  iscnp4  18842  cnpnei  18843  iscncl  18848  cnnei  18861  cnconst  18863  ordthauslem  18962  bwth  18988  1stccnp  19041  llyrest  19064  nllyrest  19065  kgenss  19091  xkoccn  19167  kqsat  19279  kqt0lem  19284  isr0  19285  fbssfi  19385  isfild  19406  filcon  19431  trfilss  19437  fgtr  19438  ufileu  19467  ufilen  19478  fmfnfmlem4  19505  fmfnfm  19506  hausflimi  19528  cnpflf2  19548  cnpflf  19549  cnflf  19550  cnpfcf  19589  cnfcf  19590  cnextcn  19614  tmdmulg  19638  clsnsg  19655  tsmsxplem1  19702  tsmsxp  19704  trust  19779  ustuqtop0  19790  ismeti  19875  isxmet2d  19877  elbl2ps  19939  elbl2  19940  xblpnfps  19945  xblpnf  19946  xbln0  19964  blin  19971  blssexps  19976  blssex  19977  blsscls2  20054  blcls  20056  blsscls  20057  metss  20058  metrest  20074  metcn  20093  metustblOLD  20130  metustbl  20131  metutopOLD  20132  psmetutop  20133  nmf2  20160  nmdvr  20226  nmoi  20282  nmoix  20283  nmoleub  20285  nghmcn  20299  xrsxmet  20361  iccntr  20373  metdsle  20403  icoopnst  20486  iocopnst  20487  icccvx  20497  pi1xfr  20602  lmmbr  20744  lmmbr2  20745  iscfil3  20759  iscau2  20763  cfilres  20782  bcthlem1  20810  bcthlem4  20813  bcthlem5  20814  rrxmet  20882  ioombl  21021  iccvolcl  21023  ioovolcl  21025  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  ig1pcl  21622  ig1prsp  21624  aannenlem1  21769  taylplem1  21803  dvtaylp  21810  relogeftb  22008  logdivlt  22045  cxpexp  22088  rpcxpcl  22096  isppw2  22428  vmappw  22429  lgslem4  22613  lgscllem  22617  lgsneg1  22634  lgsne0  22647  brbtwn2  23102  ax5seglem1  23125  ax5seglem2  23126  axcontlem4  23164  nbgraf1olem5  23305  constr3cycl  23498  grpoidinvlem3  23644  isvci  23911  nmcvcn  24041  ipval2lem2  24050  ipval2lem5  24056  sspival  24087  sspimsval  24089  isblo2  24134  nmoo0  24142  blocni  24156  isph  24173  sspph  24206  hvadd4  24389  hiassdi  24444  ocsh  24637  chj4  24889  spansncol  24922  pjjsi  25054  hoscl  25100  hodcl  25102  hoadd4  25139  homco1  25156  homulass  25157  hoadddi  25158  hoadddir  25159  unoplin  25275  adjvalval  25292  hmoplin  25297  bralnfn  25303  brafnmul  25306  lnopmi  25355  lnopcoi  25358  hmops  25375  hmopm  25376  nmophmi  25386  lnfncnbd  25412  cnlnadjlem2  25423  adjlnop  25441  adjmul  25447  adjadd  25448  branmfn  25460  kbass5  25475  kbass6  25476  leop2  25479  leopadd  25487  leopmuli  25488  pjimai  25531  atcvatlem  25740  chirredlem2  25746  mdsymlem3  25760  mdsymlem5  25762  sumdmdii  25770  sumdmdlem  25773  cdj3lem2a  25791  cdj3lem2b  25792  cdj3lem3a  25794  cdj3i  25796  xreceu  26048  toslublem  26079  tosglblem  26081  xrstos  26091  ogrpaddltbi  26133  archiabllem1a  26159  archiabllem1b  26160  archiabllem2c  26163  archiabl  26166  slmdvsdir  26183  slmdvsass  26184  ordtconlem1  26306  hasheuni  26486  ballotlemirc  26866  signspval  26905  txpcon  27073  cvmscld  27114  2cprodeq2dv  27389  dfrdg2  27560  wsuclem  27713  nobndlem8  27791  segconeu  27993  linecom  28132  linethru  28135  lineintmo  28139  heicant  28379  mblfinlem1  28381  mblfinlem3  28383  ismblfin  28385  cnambfre  28393  itg2addnclem2  28397  ftc1anclem1  28420  ftc1anclem5  28424  ftc1anclem6  28425  ftc2nc  28429  areacirclem2  28438  areacirclem4  28440  areacirclem5  28441  areacirc  28442  fnemeet2  28541  fnejoin2  28543  fzmul  28589  subspopn  28601  isbndx  28634  isbnd2  28635  isbnd3  28636  ssbnd  28640  prdstotbnd  28646  heibor1  28662  rrnmet  28681  rngonegmn1l  28708  rngohomco  28733  rngoisocnv  28740  rngoisoco  28741  crngohomfo  28759  isidlc  28768  rngoidl  28777  prnc  28820  ispridlc  28823  oddcomabszz  29238  acongtr  29274  rpnnen3lem  29333  islssfg  29376  lmhmfgsplit  29392  unxpwdom3  29401  hbtlem7  29434  sdrgacs  29511  hashgcdeq  29519  iocmbl  29541  dvconstbi  29561  otsndisj  30084  ralxfrd2  30090  el2fzo  30165  usg2wlkeq  30242  usgra2pthlem1  30253  wwlknimp  30274  wwlknred  30308  wwlknext  30309  clwwlknprop  30388  3cyclfrgrarn1  30557  3cyclfrgrarn  30558  4cycl2vnunb  30562  frgrancvvdeqlemB  30584  usgreghash2spotv  30612  2spotmdisj  30614  lcoss  30859  snlindsntorlem  30893  bnj1204  31890  cvrval2  32759  glbconxN  32862  hlrelat5N  32885  cvratlem  32905  cvrat2  32913  athgt  32940  3dim2  32952  llnn0  33000  lplnn0N  33031  lvoln0N  33075  snatpsubN  33234  paddasslem18  33321  pmod1i  33332  lhpexle2  33494  lhpexle3lem  33495  lhpexle3  33496  ldilcnv  33599  trlcnv  33649  trlnidatb  33661  cdleme32snaw  33919  cdleme32fvaw  33923  cdleme42ke  33969  cdlemeg46gf  34017  cdleme50trn12  34036  cdlemg1cex  34072  cdlemb3  34090  tgrpgrplem  34233  tgrpabl  34235  tendoplcl2  34262  tendo0pl  34275  tendoicl  34280  tendoipl  34281  cdlemkid3N  34417  tendoex  34459  erngdvlem4  34475  erngdvlem4-rN  34483  dib1dim  34650  dib1dim2  34653  dihglbcpreN  34785  dihmeetALTN  34812  dih1dimatlem  34814  dihatlat  34819
  Copyright terms: Public domain W3C validator