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

Theorem 3expia 1153
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expia  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1150 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 418 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mp3an3  1266  3gencl  2831  moi  2961  disji  4027  reusv6OLD  4561  nnsuc  4689  3optocl  4782  sossfld  5136  soisores  5840  isomin  5850  isofrlem  5853  ovmpt2s  5987  ov2gf  5988  ndmovord  6026  poxp  6243  brtpos  6259  dfsmo2  6380  smoiun  6394  smoord  6398  smogt  6400  omeulem1  6596  omeu  6599  oewordi  6605  mapvalg  6798  pmvalg  6799  elmapg  6801  xpdom3  6976  mapdom3  7049  php3  7063  unxpdomlem3  7085  isinf  7092  findcard2  7114  isfinite2  7131  ordiso  7247  cnfcom3clem  7424  r111  7463  tskwe  7599  pr2ne  7651  infxpenlem  7657  dfac8alem  7672  infdif  7851  infdif2  7852  cff1  7900  coflim  7903  cfslbn  7909  cfslb2n  7910  cofsmo  7911  cfsmolem  7912  cfcoflem  7914  fin23lem27  7970  isf32lem9  8003  isf34lem6  8022  axcc2lem  8078  domtriomlem  8084  axdc4lem  8097  zorn2lem2  8140  axdclem2  8163  konigthlem  8206  gchen1  8263  gchen2  8264  gchpwdom  8312  gchaleph  8313  winainflem  8331  tskcard  8419  gruiun  8437  gruen  8450  intgru  8452  grudomon  8455  grur1a  8457  grutsk1  8459  nqereu  8569  nqereq  8575  ltsonq  8609  prlem934  8673  reclem3pr  8689  1re  8853  axsup  8914  ltlen  8938  addid2  9011  recex  9416  lemul1a  9626  ledivmulOLD  9646  lt2msq  9656  fimaxre2  9718  zdiv  10098  zextlt  10102  prime  10108  uzind2  10120  fzind  10126  lbzbi  10322  qbtwnxr  10543  qextltlem  10545  xralrple  10548  xltneg  10560  xlt2add  10596  supxrgtmnf  10664  ixxub  10693  ixxlb  10694  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  iocssre  10745  icossre  10746  iccssre  10747  fzen  10827  expclzlem  11143  expaddz  11162  expmulz  11164  hashgadd  11375  ccatopth2  11479  shftuz  11580  cau3lem  11854  caubnd  11858  climuni  12042  lo1resb  12054  o1resb  12056  o1of2  12102  o1add  12103  o1mul  12104  o1sub  12105  eflt  12413  znnenlem  12506  moddvds  12554  dvdscmulr  12573  dvdsmulcr  12574  dvdsle  12590  divalglem8  12615  divalgb  12619  ndvdssub  12622  bitsfzo  12642  gcdcllem1  12706  gcdcllem3  12708  dvdsgcd  12738  isprm3  12783  coprm  12795  qredeu  12802  prmdvdsexpr  12811  prmexpb  12812  eulerthlem2  12866  fermltl  12868  coprimeprodsq  12878  pythagtrip  12903  pcprendvds  12909  pcpremul  12912  pcdvdsb  12937  pc2dvds  12947  4sqlem12  13019  4sqlem18  13025  vdwlem10  13053  xpslem  13491  ismred  13520  mrieqv2d  13557  iscatd  13591  isfuncd  13755  poslubd  14267  dirtr  14374  ghmrn  14712  mndodcongi  14874  oddvdsnn0  14875  oddvds  14878  odcl2  14894  odhash3  14903  gexdvds  14911  pgpfi  14932  lsmss1b  14992  lsmss2b  14994  efgsrel  15059  efgred  15073  cntzcmn  15152  cyggenod  15187  lt6abl  15197  gsumcom2  15242  pgpfac1lem2  15326  pgpfac1lem3  15328  dvdsunit  15461  unitmulclb  15463  irredrmul  15505  isabvd  15601  lmodvsdi  15666  lss0cl  15720  islbs3  15924  lbsextlem2  15928  mvrf1  16186  xrsdsreclblem  16433  opnnei  16873  neindisj2  16876  cncls2  17018  cncls  17019  cnntr  17020  cnpresti  17032  cnprest  17033  lmcnp  17048  isreg2  17121  ordthauslem  17127  uncon  17171  2ndc1stc  17193  kgen2ss  17266  ptclsg  17325  cnmptcom  17388  kqfvima  17437  hmeof1o  17471  fbncp  17550  fbfinnfr  17552  trfbas2  17554  isufil2  17619  ufprim  17620  trufil  17621  filufint  17631  hausflim  17692  flimrest  17694  flimcls  17696  cnpfcf  17752  alexsubALT  17761  tmdgsum  17794  opnsubg  17806  cldsubg  17809  divstgpopn  17818  tsmsxp  17853  blpnf  17970  blss  17988  blssec  17997  neibl  18063  prdsxmslem2  18091  xrsmopn  18334  metnrm  18382  climcncf  18420  iccpnfhmeo  18459  xrhmeo  18460  bndth  18472  cphsqrcl3  18639  iscau2  18719  iscmet3lem2  18734  bcthlem5  18766  bcth3  18769  ishl2  18803  ivthlem1  18827  cmmbl  18908  iundisj2  18922  voliunlem2  18924  mbfaddlem  19031  itg2itg1  19107  itg2seq  19113  itg2mulclem  19117  cnplimc  19253  dvres2  19278  deg1nn0clb  19492  deg1lt0  19493  deg1ge  19500  plypf1  19610  plyadd  19615  plymul  19616  coeeu  19623  dgrub2  19633  coeidlem  19635  coeid3  19638  coemullem  19647  coe11  19650  coemulhi  19651  coemulc  19652  dgreq0  19662  dgrlt  19663  dgradd2  19665  vieta1lem2  19707  sineq0  19905  tanord1  19915  tanord  19916  cxpeq0  20041  cxpmul2z  20054  cxpcn3lem  20103  angpieqvd  20144  o1cxp  20285  scvxcvx  20296  chtublem  20466  bposlem3  20541  lgsqr  20601  dchrisumlema  20653  dchrisumlem2  20655  ostth2lem3  20800  lpni  20862  gxnn0neg  20946  gxnn0suc  20947  gxcl  20948  gxneg  20949  gxcom  20952  gxinv  20953  gxsuc  20955  gxnn0add  20957  gxadd  20958  gxnn0mul  20960  gxmul  20961  ipasslem5  21429  htthlem  21513  omlsii  21998  spansni  22152  spansneleq  22165  elspansn4  22168  sumspansn  22244  homco1  22397  homulass  22398  mdsl0  22906  ssdmd1  22909  ssdmd2  22910  cvdmd  22933  chirredlem2  22987  atdmd  22994  atmd2  22996  isoun  23257  iocinioc2  23287  disjif  23370  disjif2  23373  iundisj2fi  23379  iundisj2f  23381  logccne0  23412  measinblem  23562  measres  23564  measdivcstOLD  23566  measdivcst  23567  mbfmco2  23585  indpi1  23620  orvclteinc  23691  cvmlift2lem10  23858  ghomf1olem  24016  nodense  24414  dfrdg4  24560  brbtwn2  24605  axpasch  24641  axcontlem4  24667  axcontlem5  24668  brcolinear2  24753  brsegle2  24804  limsucncmpi  24956  ee7.2aOLD  24972  areacirc  25034  rspc2edv  25066  uninqs  25142  domintreflemb  25165  injsurinj  25252  repcpwti  25264  cbcpcp  25265  prl1  25271  oriso  25317  ubos  25359  curgrpact  25475  ltrran2  25506  ltrooo  25507  fldi  25530  svli2  25587  elioo1t3  25605  intopcoaconb  25643  limptlimpr2lem2  25678  islimrs4  25685  lvsovso  25729  negveud  25771  negveudr  25772  clsmulrv  25786  intvconlem1  25806  cmpassoh  25904  issrc  25970  clscnc  26113  isconcl6a  26206  nn0prpw  26342  ntruni  26348  clsint2  26350  fnessref  26396  fnemeet2  26419  fnejoin2  26421  filbcmb  26535  mettrifi  26576  heiborlem8  26645  heiborlem10  26647  heibor  26648  riscer  26722  igenval2  26794  oddcomabszz  27132  jm2.19lem4  27188  fiuneneq  27616  idomsubgmo  27617  addrcom  27783  stoweidlem26  27878  stoweidlem34  27886  int3  28689  suctrALTcf  29014  suctrALT3  29016  suctrALT4  29020  chordthmALT  29026  bnj605  29255  bnj607  29264  bnj964  29291  bnj1033  29315  bnj1128  29336  bnj1137  29341  bnj1136  29343  bnj1413  29381  bnj60  29408  lshpcmp  29800  eqlkr  29911  lkrlsp2  29915  lkrshp  29917  cvrnbtwn2  30087  cvlexch3  30144  cvlexch4N  30145  cvlatexchb1  30146  cvlsupr3  30156  exatleN  30215  cvratlem  30232  atcvrj2b  30243  cvrat3  30253  cvrat4  30254  athgt  30267  ps-1  30288  ps-2  30289  3atlem5  30298  3at  30301  llnneat  30325  llnmlplnN  30350  lplnneat  30356  lplnnelln  30357  islpln2a  30359  lplnriaN  30361  lplnribN  30362  lplnexllnN  30375  2llnjaN  30377  lvolnle3at  30393  lvolneatN  30399  lvolnelln  30400  lvolnelpln  30401  islvol2aN  30403  dalem62  30545  pmapglb2N  30582  pmapglb2xN  30583  lncmp  30594  paddasslem14  30644  paddasslem15  30645  pmod2iN  30660  hlmod1i  30667  pclfinclN  30761  osumcllem8N  30774  pexmidlem4N  30784  pl42lem1N  30790  pl42lem4N  30793  lhpexle1  30819  lhpexle2lem  30820  lhpmcvr5N  30838  lhpmcvr6N  30839  ltrneq  30960  trlnidatb  30988  cdleme0ex2N  31035  cdleme27a  31178  cdleme17d3  31307  cdlemeg46gfre  31343  cdleme48gfv1  31347  cdlemeg49lebilem  31350  cdlemf2  31373  cdlemf  31374  cdlemfnid  31375  trlord  31380  cdlemg31c  31510  cdlemg35  31524  trlcone  31539  tendoeq2  31585  cdlemj3  31634  cdlemk26b-3  31716  cdlemk33N  31720  cdleml3N  31789  cdlemn  32024  dih1dimb2  32053  dihord5apre  32074  dihmeetlem1N  32102  dihglblem5apreN  32103  dihglblem2N  32106  dihglblem3N  32107  dihmeetlem13N  32131  dihmeetlem15N  32133  dihatexv  32150  hdmap14lem12  32694
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator