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  2785  moi2  3187  sbc3ie  3305  2if2  3895  preq12bg  4115  prel12g  4116  reuhypd  4584  otsndisj  4661  fvtp1g  6066  f1imass  6117  weisoeq  6198  f1ofveu  6237  f1ocnvfv3  6238  curry1f  6838  curry2f  6840  funsssuppss  6889  tfrlem11  7054  oalimcl  7209  oeordsuc  7243  oelim2  7244  nneob  7301  mapxpen  7684  findcard  7756  wemaplem3  8009  en2eqpr  8383  infxpabs  8586  infxp  8589  cfflb  8633  cfsmolem  8644  isf32lem12  8738  fin1a2lem9  8782  fin1a2s  8788  axcc3  8812  axdc3lem4  8827  zornn0g  8879  pwfseqlem4  9031  tskwun  9153  tskint  9154  tskxp  9156  tskmap  9157  gruf  9180  gruwun  9182  grutsk1  9190  addcanpi  9268  ltapi  9272  mul4  9746  add4  9793  2addsub  9833  addsubeq4  9834  muladd  9995  ltleadd  10041  receu  10201  p1le  10392  lemul12b  10406  lbinf  10503  lbinfmOLD  10504  zdiv  10950  fzind  10977  fnn0ind  10978  uzss  11123  zbtwnre  11206  qmulcl  11226  qreccl  11228  xrlttr  11383  xaddass  11479  xmulasslem3  11516  xmulass  11517  xadddilem  11524  xrsupsslem  11536  xrinfmsslem  11537  supxrunb1  11549  ixxin  11596  ioo0  11605  ico0  11626  ioc0  11627  icc0  11628  iooshf  11657  prunioo  11705  ioojoin  11707  elfz5  11736  elfz0fzfz0  11839  elfzonelfzo  11954  fzind2  11966  mulexpz  12255  expsub  12263  digit2  12348  digit1  12349  facndiv  12416  faclbnd4lem4  12424  faclbnd4  12425  faclbnd5  12426  bccmpl  12437  bcval5  12446  bcpasc  12449  hashunx  12508  ccatrn  12674  swrdccat1  12752  swrdccat2  12753  swrdswrd  12755  cats1un  12771  crim  13115  absmax  13329  ello12r  13517  elo12r  13528  climshftlem  13574  2sumeq2dv  13707  expcnv  13858  2cprodeq2dv  13915  rpnnen2lem7  14209  dvdsval3  14245  dvdsnegb  14256  muldvds1  14263  muldvds2  14264  dvdscmul  14265  dvdsmulc  14266  dvdsmulcr  14268  dvds2ln  14269  divalgb  14321  ndvdssub  14324  gcddiv  14453  lcmfval  14527  lcmfvalOLD  14531  lcmfcl  14537  dvdslcmf  14540  rpexp1i  14609  phiprmpw  14660  pythagtriplem1  14702  pockthg  14786  infpnlem1  14790  4sqlem3  14830  0ramcl  14917  firest  15267  imasaddfnlem  15370  imasleval  15383  xpsfrn2  15412  mrerintcl  15439  iscatd  15515  fullestrcsetc  15972  fullsetcestrc  15987  clatleglb  16308  mreclatBAD  16369  pslem  16388  mrcmndind  16549  grplmulf1o  16664  grplactcnv  16690  mulgnn0subcl  16707  mulgsubcl  16708  mulgdir  16719  issubg2  16768  issubgrpd2  16769  cycsubgcl  16779  cycsubgss  16780  nmzsubg  16794  eqgen  16806  ghmmulg  16831  conjghm  16849  symgfixfo  17016  odeq  17135  odval2  17136  odf1  17149  dfod2  17151  gexdvds  17171  gexdvds2  17173  gexcl2  17177  gexdvds3  17178  sylow2blem2  17209  efgsp1  17323  efgrelexlemb  17336  mulgmhm  17404  mulgghm  17405  iscyggen2  17452  iscyg3  17457  srglmhm  17704  srgrmhm  17705  ringlghm  17768  ringrghm  17769  gsumdixp  17773  dvdsrcl2  17814  crngunit  17826  kerf1hrm  17907  subrgugrp  17963  cntzsubr  17976  lmodvsdir  18051  lmodvsass  18052  lmodvsghm  18085  lsssubg  18116  lss1d  18122  islbs2  18313  lidlsubg  18374  lidlsubcl  18375  quscrng  18400  lpigen  18416  xrsdsreval  18949  expghm  19002  mulgghm2  19003  ip0r  19139  obs2ss  19227  islindf3  19319  scmatscm  19473  scmataddcl  19476  scmatsubcl  19477  scmatfo  19490  matunit  19638  cpmatelimp  19671  cpmatelimp2  19673  cpmatinvcl  19676  cpmatmcl  19678  mat2pmatf  19687  m2cpmf  19701  cpm2mf  19711  m2cpmfo  19715  m2cpminv  19719  decpmataa0  19727  pm2mpf  19757  pm2mpf1  19758  idpm2idmp  19760  pm2mpfo  19773  elcls2  20025  opnnei  20071  innei  20076  iscnp4  20214  cnpnei  20215  iscncl  20220  cnnei  20233  cnconst  20235  ordthauslem  20334  bwth  20360  1stccnp  20412  llyrest  20435  nllyrest  20436  kgenss  20493  xkoccn  20569  kqsat  20681  kqt0lem  20686  isr0  20687  fbssfi  20787  isfild  20808  filcon  20833  trfilss  20839  fgtr  20840  ufileu  20869  ufilen  20880  fmfnfmlem4  20907  fmfnfm  20908  hausflimi  20930  cnpflf2  20950  cnpflf  20951  cnflf  20952  cnpfcf  20991  cnfcf  20992  cnextcn  21017  tmdmulg  21042  clsnsg  21059  tsmsxplem1  21102  tsmsxp  21104  trust  21179  ustuqtop0  21190  ismeti  21275  isxmet2d  21277  elbl2ps  21339  elbl2  21340  xblpnfps  21345  xblpnf  21346  xbln0  21364  blin  21371  blssexps  21376  blssex  21377  blsscls2  21454  blcls  21456  blsscls  21457  metss  21458  metrest  21474  metcn  21493  metustbl  21516  psmetutop  21517  nmf2  21542  nmdvr  21608  nmoi  21668  nmoix  21669  nmoleub  21671  nmoiOLD  21684  nmoixOLD  21685  nmoleubOLD  21687  nghmcn  21701  xrsxmet  21762  iccntr  21774  metdsle  21804  metdsleOLD  21819  icoopnst  21902  iocopnst  21903  icccvx  21913  pi1xfr  22021  lmmbr  22163  lmmbr2  22164  iscfil3  22178  iscau2  22182  cfilres  22201  bcthlem1  22227  bcthlem4  22230  bcthlem5  22231  rrxmet  22297  ioombl  22453  iccvolcl  22455  ioovolcl  22457  mbfi1fseqlem3  22610  mbfi1fseqlem4  22611  mbfi1fseqlem5  22612  ig1pcl  23062  ig1prsp  23064  ig1pclOLD  23068  ig1prspOLD  23070  aannenlem1  23219  taylplem1  23253  dvtaylp  23260  relogeftb  23469  logdivlt  23505  cxpexp  23548  rpcxpcl  23556  isppw2  23977  vmappw  23978  lgslem4  24162  lgscllem  24166  lgsneg1  24183  lgsne0  24196  cgraswap  24797  brbtwn2  24870  ax5seglem1  24893  ax5seglem2  24894  axcontlem4  24932  nbgraf1olem5  25108  constr3cycl  25324  wwlknimp  25350  usg2wlkeq  25371  wwlknred  25386  wwlknext  25387  clwwlknprop  25435  3cyclfrgrarn1  25675  3cyclfrgrarn  25676  4cycl2vnunb  25680  frgrancvvdeqlemB  25701  usgreghash2spotv  25729  2spotmdisj  25731  grpoidinvlem3  25869  isvci  26136  nmcvcn  26266  ipval2lem2  26275  ipval2lem5  26281  sspival  26312  sspimsval  26314  isblo2  26359  nmoo0  26367  blocni  26381  isph  26398  sspph  26431  hvadd4  26624  hiassdi  26679  ocsh  26871  chj4  27123  spansncol  27156  pjjsi  27288  hoscl  27333  hodcl  27335  hoadd4  27372  homco1  27389  homulass  27390  hoadddi  27391  hoadddir  27392  unoplin  27508  adjvalval  27525  hmoplin  27530  bralnfn  27536  brafnmul  27539  lnopmi  27588  lnopcoi  27591  hmops  27608  hmopm  27609  nmophmi  27619  lnfncnbd  27645  cnlnadjlem2  27656  adjlnop  27674  adjmul  27680  adjadd  27681  branmfn  27693  kbass5  27708  kbass6  27709  leop2  27712  leopadd  27720  leopmuli  27721  pjimai  27764  atcvatlem  27973  chirredlem2  27979  mdsymlem3  27993  mdsymlem5  27995  sumdmdii  28003  sumdmdlem  28006  cdj3lem2a  28024  cdj3lem2b  28025  cdj3lem3a  28027  cdj3i  28029  xreceu  28335  toslublem  28372  tosglblem  28374  ogrpaddltbi  28426  archiabllem1b  28453  archiabllem2c  28456  archiabl  28459  slmdvsdir  28476  slmdvsass  28477  pstmxmet  28645  ordtconlem1  28675  hasheuni  28851  omsf  29065  omsfOLD  29069  ballotlemirc  29309  ballotlemircOLD  29347  signswmnd  29391  bnj1204  29766  txpcon  29900  cvmscld  29941  elmpps  30156  dfrdg2  30386  wsuclem  30452  nobndlem8  30530  segconeu  30720  linecom  30859  linethru  30862  lineintmo  30866  fnemeet2  30965  fnejoin2  30967  heicant  31876  mblfinlem1  31878  mblfinlem3  31880  ismblfin  31882  cnambfre  31890  itg2addnclem2  31895  ftc1anclem1  31918  ftc1anclem5  31922  ftc1anclem6  31923  ftc2nc  31927  areacirclem2  31934  areacirclem4  31936  areacirclem5  31937  areacirc  31938  fzmul  31970  subspopn  31982  isbndx  32015  isbnd2  32016  isbnd3  32017  ssbnd  32021  prdstotbnd  32027  heibor1  32043  rrnmet  32062  rngonegmn1l  32089  rngohomco  32114  rngoisocnv  32121  rngoisoco  32122  crngohomfo  32140  isidlc  32149  rngoidl  32158  prnc  32201  ispridlc  32204  cvrval2  32746  glbconxN  32849  hlrelat5N  32872  cvratlem  32892  cvrat2  32900  athgt  32927  3dim2  32939  llnn0  32987  lplnn0N  33018  lvoln0N  33062  snatpsubN  33221  paddasslem18  33308  pmod1i  33319  lhpexle2  33481  lhpexle3lem  33482  lhpexle3  33483  ldilcnv  33586  trlcnv  33637  trlnidatb  33649  cdleme32snaw  33908  cdleme32fvaw  33912  cdleme42ke  33958  cdlemeg46gf  34006  cdleme50trn12  34025  cdlemg1cex  34061  cdlemb3  34079  tgrpgrplem  34222  tgrpabl  34224  tendoplcl2  34251  tendo0pl  34264  tendoicl  34269  tendoipl  34270  cdlemkid3N  34406  tendoex  34448  erngdvlem4  34464  erngdvlem4-rN  34472  dib1dim  34639  dib1dim2  34642  dihglbcpreN  34774  dihmeetALTN  34801  dih1dimatlem  34803  dihatlat  34808  oddcomabszz  35699  acongtr  35735  rpnnen3lem  35793  islssfg  35835  lmhmfgsplit  35851  unxpwdom3  35860  hbtlem7  35891  sdrgacs  35974  hashgcdeq  35982  iocmbl  36004  ss2iundf  36158  nzss  36573  dvconstbi  36590  bccbc  36601  uzmptshftfval  36602  iccdifprioo  37503  dvnmul  37695  fourierdlem74  37921  fourierdlem75  37922  sge0iunmptlemfi  38100  sge0iunmptlemre  38102  sge0iunmpt  38105  sge0xp  38116  volico  38204  nnsum4primesodd  38698  nnsum4primesoddALTV  38699  pfxccat1  38758  ralxfrd2  38809  usgra2pthlem1  39252  rnghmsubcsetclem2  39563  rhmsubcsetclem2  39609  rhmsubcrngclem2  39615  lcoss  39816  snlindsntorlem  39850  aacllem  40127
  Copyright terms: Public domain W3C validator