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

Theorem 3expia 1199
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 1196 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 427 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  mp3an3  1315  3gencl  3090  moi  3231  disji  4382  3optocl  4901  sossfld  5270  f1oresrab  6041  soisores  6205  isomin  6215  isofrlem  6218  ovmpt2s  6406  ov2gf  6407  ndmovord  6445  nnsuc  6699  poxp  6895  brtpos  6966  dfsmo2  7050  smoiun  7064  smoord  7068  smogt  7070  omeulem1  7267  omeu  7270  oewordi  7276  uniinqs  7427  mapvalg  7466  pmvalg  7467  elmapg  7469  xpdom3  7652  mapdom3  7726  php3  7740  unxpdomlem3  7760  isinf  7767  findcard2  7793  isfinite2  7811  ordiso  7974  cnfcom3clem  8180  cnfcom3clemOLD  8188  r111  8224  tskwe  8362  pr2ne  8414  infxpenlem  8422  dfac8alem  8441  infdif  8620  infdif2  8621  cff1  8669  coflim  8672  cfslbn  8678  cfslb2n  8679  cofsmo  8680  cfsmolem  8681  cfcoflem  8683  fin23lem27  8739  isf32lem9  8772  isf34lem6  8791  axcc2lem  8847  domtriomlem  8853  axdc4lem  8866  zorn2lem2  8908  axdclem2  8931  konigthlem  8974  gchen1  9032  gchen2  9033  gchpwdom  9077  gchaleph  9078  winainflem  9100  tskcard  9188  gruiun  9206  gruen  9219  intgru  9221  grudomon  9224  grur1a  9226  grutsk1  9228  nqereu  9336  nqereq  9342  ltsonq  9376  prlem934  9440  reclem3pr  9456  1re  9624  axsup  9690  ltlen  9716  addid2  9796  recex  10221  lemul1a  10436  lt2msq  10468  fimaxre2  10530  zdiv  10973  zextlt  10977  prime  10983  uzind2  10995  fzind  11000  lbzbi  11214  qbtwnxr  11451  qextltlem  11453  xralrple  11456  xltneg  11468  xlt2add  11504  supxrgtmnf  11573  ixxub  11602  ixxlb  11603  ioo0  11606  ico0  11627  ioc0  11628  icc0  11629  iocssre  11656  icossre  11657  iccssre  11658  fzen  11755  expclzlem  12232  expaddz  12252  expmulz  12254  hashgadd  12491  elovmpt2wrd  12634  ccatopth2  12750  shftuz  13049  cau3lem  13334  caubnd  13338  climuni  13522  lo1resb  13534  o1resb  13536  o1of2  13582  o1add  13583  o1mul  13584  o1sub  13585  ntrivcvgmul  13861  eflt  14059  znnenlem  14152  moddvds  14200  dvdscmulr  14219  dvdsmulcr  14220  dvdsle  14238  divalglem8  14265  divalgb  14269  ndvdssub  14272  bitsfzo  14292  gcdcllem1  14356  gcdcllem3  14358  dvdsgcd  14388  isprm3  14433  coprm  14448  qredeu  14455  prmdvdsexpr  14464  prmexpb  14465  eulerthlem2  14519  fermltl  14521  coprimeprodsq  14540  pythagtrip  14565  pcprendvds  14571  pcpremul  14574  pcdvdsb  14599  pc2dvds  14609  4sqlem12  14681  4sqlem18  14687  vdwlem10  14715  cshwshashlem3  14789  xpslem  15185  ismred  15214  mrieqv2d  15251  iscatd  15285  isfuncd  15476  fthestrcsetc  15741  fthsetcestrc  15756  poslubd  16100  dirtr  16188  ghmrn  16602  pmtrprfv3  16801  mndodcongi  16889  oddvdsnn0  16890  oddvds  16893  odcl2  16909  odhash3  16918  gexdvds  16926  pgpfi  16947  lsmss1b  17007  lsmss2b  17009  efgsrel  17074  efgred  17088  cntzcmn  17170  cyggenod  17209  lt6abl  17219  gsumcom2  17322  pgpfac1lem2  17444  pgpfac1lem3  17446  dvdsunit  17630  unitmulclb  17632  irredrmul  17674  isabvd  17787  lmodvsdi  17853  lss0cl  17911  islbs3  18119  lbsextlem2  18123  mvrf1  18399  coe1fzgsumd  18662  gsummoncoe1  18664  evl1gsumd  18711  xrsdsreclblem  18782  scmataddcl  19308  scmatsubcl  19309  mdetunilem9  19412  mdetuni0  19413  mdetmul  19415  m2cpmrngiso  19549  pm2mpf1  19590  opnnei  19912  neindisj2  19915  cncls2  20065  cncls  20066  cnntr  20067  cnpresti  20080  cnprest  20081  lmcnp  20096  isreg2  20169  ordthauslem  20175  uncon  20220  2ndc1stc  20242  kgen2ss  20346  ptclsg  20406  cnmptcom  20469  kqfvima  20521  hmeof1o  20555  fbncp  20630  fbfinnfr  20632  trfbas2  20634  isufil2  20699  ufprim  20700  trufil  20701  filufint  20711  hausflim  20772  flimrest  20774  flimcls  20776  cnpfcf  20832  alexsubALT  20841  tmdgsum  20884  opnsubg  20896  cldsubg  20899  qustgpopn  20908  tsmsxp  20947  blpnf  21190  blssps  21217  blss  21218  blssec  21228  neibl  21294  prdsxmslem2  21322  xrsmopn  21607  metnrm  21656  climcncf  21694  iccpnfhmeo  21735  xrhmeo  21736  bndth  21748  cphsqrtcl3  21924  iscau2  22006  iscmet3lem2  22021  bcthlem5  22057  bcth3  22060  ishl2  22100  ivthlem1  22153  cmmbl  22235  iundisj2  22249  voliunlem2  22251  mbfaddlem  22357  itg2itg1  22433  itg2seq  22439  itg2mulclem  22443  cnplimc  22581  dvres2  22606  deg1nn0clb  22780  deg1lt0  22781  deg1ge  22789  plypf1  22899  plyadd  22904  plymul  22905  coeeu  22912  dgrub2  22922  coeidlem  22924  coeid3  22927  coemullem  22937  coe11  22940  coemulhi  22941  coemulc  22942  dgreq0  22952  dgrlt  22953  dgradd2  22955  vieta1lem2  22997  sineq0  23204  tanord1  23214  tanord  23215  logccne0  23256  cxpeq0  23351  cxpmul2z  23364  cxpcn3lem  23415  relogbzcl  23439  angpieqvd  23485  o1cxp  23628  scvxcvx  23639  chtublem  23865  bposlem3  23940  lgsqr  24000  dchrisumlema  24052  dchrisumlem2  24054  ostth2lem3  24199  tghilberti2  24401  f1otrg  24578  brbtwn2  24612  axpasch  24648  axcontlem4  24674  axcontlem5  24675  sizeusglecusg  24890  wwlkextproplem3  25147  lpni  25585  gxnn0neg  25665  gxnn0suc  25666  gxcl  25667  gxneg  25668  gxcom  25671  gxinv  25672  gxsuc  25674  gxnn0add  25676  gxadd  25677  gxnn0mul  25679  gxmul  25680  ipasslem5  26150  htthlem  26234  omlsii  26721  spansni  26875  spansneleq  26888  elspansn4  26891  sumspansn  26967  homco1  27119  homulass  27120  mdsl0  27628  ssdmd1  27631  ssdmd2  27632  cvdmd  27655  chirredlem2  27709  atdmd  27716  atmd2  27718  disjif  27856  iundisj2f  27868  isoun  27950  padct  27978  iocinioc2  28024  iundisj2fi  28036  archiabllem1a  28173  archiabllem2a  28176  slmdvsdi  28196  ordtconlem1  28345  indpi1  28455  measinblem  28654  measres  28656  measdivcstOLD  28658  mbfmco2  28699  orvclteinc  28906  sgn3da  28972  sgnnbi  28976  sgnpbi  28977  bnj605  29279  bnj607  29288  bnj964  29315  bnj1033  29339  bnj1128  29360  bnj1137  29365  bnj1136  29367  bnj1413  29405  bnj60  29432  cvmlift2lem10  29596  msubvrs  29759  ghomf1olem  29873  wsuclem  30068  nodense  30136  dfrdg4  30276  brcolinear2  30383  brsegle2  30434  nn0prpw  30538  ntruni  30542  clsint2  30544  fnessref  30572  fnemeet2  30582  fnejoin2  30584  limsucncmpi  30664  ee7.2aOLD  30680  dissneqlem  31243  isbasisrelowllem1  31259  isbasisrelowllem2  31260  icoreclin  31261  areacirc  31463  filbcmb  31493  mettrifi  31512  heiborlem8  31576  heiborlem10  31578  heibor  31579  riscer  31653  igenval2  31725  lshpcmp  31986  eqlkr  32097  lkrlsp2  32101  lkrshp  32103  cvrnbtwn2  32273  cvlexch3  32330  cvlexch4N  32331  cvlatexchb1  32332  cvlsupr3  32342  exatleN  32401  cvratlem  32418  atcvrj2b  32429  cvrat3  32439  cvrat4  32440  athgt  32453  ps-1  32474  ps-2  32475  3atlem5  32484  3at  32487  llnneat  32511  llnmlplnN  32536  lplnneat  32542  lplnnelln  32543  islpln2a  32545  lplnriaN  32547  lplnribN  32548  lplnexllnN  32561  2llnjaN  32563  lvolnle3at  32579  lvolneatN  32585  lvolnelln  32586  lvolnelpln  32587  islvol2aN  32589  dalem62  32731  pmapglb2N  32768  pmapglb2xN  32769  lncmp  32780  paddasslem14  32830  paddasslem15  32831  pmod2iN  32846  hlmod1i  32853  pclfinclN  32947  osumcllem8N  32960  pexmidlem4N  32970  pl42lem1N  32976  pl42lem4N  32979  lhpexle1  33005  lhpexle2lem  33006  lhpmcvr5N  33024  lhpmcvr6N  33025  ltrneq  33146  trlnidatb  33175  cdleme0ex2N  33222  cdleme27a  33366  cdleme17d3  33495  cdlemeg46gfre  33531  cdleme48gfv1  33535  cdlemeg49lebilem  33538  cdlemf2  33561  cdlemf  33562  cdlemfnid  33563  trlord  33568  cdlemg31c  33698  cdlemg35  33712  trlcone  33727  tendoeq2  33773  cdlemj3  33822  cdlemk26b-3  33904  cdlemk33N  33908  cdleml3N  33977  cdlemn  34212  dih1dimb2  34241  dihord5apre  34262  dihmeetlem1N  34290  dihglblem5apreN  34291  dihglblem2N  34294  dihglblem3N  34295  dihmeetlem13N  34319  dihmeetlem15N  34321  dihatexv  34338  hdmap14lem12  34882  oddcomabszz  35221  jm2.19lem4  35276  fiuneneq  35498  idomsubgmo  35499  pwinfi3  35594  lcmgcdlem  36040  binomcxplemnn0  36082  addrcom  36212  int3  36402  suctrALT  36636  suctrALTcf  36733  suctrALT3  36735  chordthmALT  36744  iunconlem2  36746  stoweidlem26  37157  stoweidlem34  37165  nnsgrp  38115  ply1mulgsumlem1  38478
  Copyright terms: Public domain W3C validator