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  2819  moi  2949  disji  4012  reusv6OLD  4544  nnsuc  4672  3optocl  4765  sossfld  5119  soisores  5786  isomin  5796  isofrlem  5799  ovmpt2s  5933  ov2gf  5934  ndmovord  5972  poxp  6189  brtpos  6205  dfsmo2  6360  smoiun  6374  smoord  6378  smogt  6380  omeulem1  6576  omeu  6579  oewordi  6585  mapvalg  6778  pmvalg  6779  elmapg  6781  xpdom3  6956  mapdom3  7029  php3  7043  unxpdomlem3  7065  isinf  7072  findcard2  7094  isfinite2  7111  ordiso  7227  cnfcom3clem  7404  r111  7443  tskwe  7579  pr2ne  7631  infxpenlem  7637  dfac8alem  7652  infdif  7831  infdif2  7832  cff1  7880  coflim  7883  cfslbn  7889  cfslb2n  7890  cofsmo  7891  cfsmolem  7892  cfcoflem  7894  fin23lem27  7950  isf32lem9  7983  isf34lem6  8002  axcc2lem  8058  domtriomlem  8064  axdc4lem  8077  zorn2lem2  8120  axdclem2  8143  konigthlem  8186  gchen1  8243  gchen2  8244  gchpwdom  8292  gchaleph  8293  winainflem  8311  tskcard  8399  gruiun  8417  gruen  8430  intgru  8432  grudomon  8435  grur1a  8437  grutsk1  8439  nqereu  8549  nqereq  8555  ltsonq  8589  prlem934  8653  reclem3pr  8669  1re  8833  axsup  8894  ltlen  8918  addid2  8991  recex  9396  lemul1a  9606  ledivmulOLD  9626  lt2msq  9636  fimaxre2  9698  zdiv  10078  zextlt  10082  prime  10088  uzind2  10100  fzind  10105  lbzbi  10302  qbtwnxr  10523  qextltlem  10525  xralrple  10528  xltneg  10540  xlt2add  10576  supxrgtmnf  10644  ixxub  10673  ixxlb  10674  ioo0  10677  ico0  10698  ioc0  10699  icc0  10700  iocssre  10725  icossre  10726  iccssre  10727  fzen  10807  expclzlem  11123  expaddz  11142  expmulz  11144  hashgadd  11355  ccatopth2  11459  shftuz  11560  cau3lem  11834  caubnd  11838  climuni  12022  lo1resb  12034  o1resb  12036  o1of2  12082  o1add  12083  o1mul  12084  o1sub  12085  eflt  12393  znnenlem  12486  moddvds  12534  dvdscmulr  12553  dvdsmulcr  12554  dvdsle  12570  divalglem8  12595  divalgb  12599  ndvdssub  12602  bitsfzo  12622  gcdcllem1  12686  gcdcllem3  12688  dvdsgcd  12718  isprm3  12763  coprm  12775  qredeu  12782  prmdvdsexpr  12791  prmexpb  12792  eulerthlem2  12846  fermltl  12848  coprimeprodsq  12858  pythagtrip  12883  pcprendvds  12889  pcpremul  12892  pcdvdsb  12917  pc2dvds  12927  4sqlem12  12999  4sqlem18  13005  vdwlem10  13033  xpslem  13471  ismred  13500  mrieqv2d  13537  iscatd  13571  isfuncd  13735  poslubd  14247  dirtr  14354  ghmrn  14692  mndodcongi  14854  oddvdsnn0  14855  oddvds  14858  odcl2  14874  odhash3  14883  gexdvds  14891  pgpfi  14912  lsmss1b  14972  lsmss2b  14974  efgsrel  15039  efgred  15053  cntzcmn  15132  cyggenod  15167  lt6abl  15177  gsumcom2  15222  pgpfac1lem2  15306  pgpfac1lem3  15308  dvdsunit  15441  unitmulclb  15443  irredrmul  15485  isabvd  15581  lmodvsdi  15646  lss0cl  15700  islbs3  15904  lbsextlem2  15908  mvrf1  16166  xrsdsreclblem  16413  opnnei  16853  neindisj2  16856  cncls2  16998  cncls  16999  cnntr  17000  cnpresti  17012  cnprest  17013  lmcnp  17028  isreg2  17101  ordthauslem  17107  uncon  17151  2ndc1stc  17173  kgen2ss  17246  ptclsg  17305  cnmptcom  17368  kqfvima  17417  hmeof1o  17451  fbncp  17530  fbfinnfr  17532  trfbas2  17534  isufil2  17599  ufprim  17600  trufil  17601  filufint  17611  hausflim  17672  flimrest  17674  flimcls  17676  cnpfcf  17732  alexsubALT  17741  tmdgsum  17774  opnsubg  17786  cldsubg  17789  divstgpopn  17798  tsmsxp  17833  blpnf  17950  blss  17968  blssec  17977  neibl  18043  prdsxmslem2  18071  xrsmopn  18314  metnrm  18362  climcncf  18400  iccpnfhmeo  18439  xrhmeo  18440  bndth  18452  cphsqrcl3  18619  iscau2  18699  iscmet3lem2  18714  bcthlem5  18746  bcth3  18749  ishl2  18783  ivthlem1  18807  cmmbl  18888  iundisj2  18902  voliunlem2  18904  mbfaddlem  19011  itg2itg1  19087  itg2seq  19093  itg2mulclem  19097  cnplimc  19233  dvres2  19258  deg1nn0clb  19472  deg1lt0  19473  deg1ge  19480  plypf1  19590  plyadd  19595  plymul  19596  coeeu  19603  dgrub2  19613  coeidlem  19615  coeid3  19618  coemullem  19627  coe11  19630  coemulhi  19631  coemulc  19632  dgreq0  19642  dgrlt  19643  dgradd2  19645  vieta1lem2  19687  sineq0  19885  tanord1  19895  tanord  19896  cxpeq0  20021  cxpmul2z  20034  cxpcn3lem  20083  angpieqvd  20124  o1cxp  20265  scvxcvx  20276  chtublem  20446  bposlem3  20521  lgsqr  20581  dchrisumlema  20633  dchrisumlem2  20635  ostth2lem3  20780  lpni  20840  gxnn0neg  20924  gxnn0suc  20925  gxcl  20926  gxneg  20927  gxcom  20930  gxinv  20931  gxsuc  20933  gxnn0add  20935  gxadd  20936  gxnn0mul  20938  gxmul  20939  ipasslem5  21407  htthlem  21491  omlsii  21978  spansni  22132  spansneleq  22145  elspansn4  22148  sumspansn  22224  homco1  22377  homulass  22378  mdsl0  22886  ssdmd1  22889  ssdmd2  22890  cvdmd  22913  chirredlem2  22967  atdmd  22974  atmd2  22976  cvmlift2lem10  23250  ghomf1olem  23408  axdense  23747  axfelem22  23771  dfrdg4  23898  brbtwn2  23943  axpasch  23979  axcontlem4  24005  axcontlem5  24006  brcolinear2  24091  brsegle2  24142  limsucncmpi  24294  ee7.2aOLD  24310  areacirc  24341  rspc2edv  24373  uninqs  24449  domintreflemb  24472  injsurinj  24560  repcpwti  24572  cbcpcp  24573  prl1  24579  oriso  24625  ubos  24667  curgrpact  24783  ltrran2  24814  ltrooo  24815  fldi  24838  svli2  24895  elioo1t3  24913  intopcoaconb  24951  limptlimpr2lem2  24986  islimrs4  24993  lvsovso  25037  negveud  25079  negveudr  25080  clsmulrv  25094  intvconlem1  25114  cmpassoh  25212  issrc  25278  clscnc  25421  isconcl6a  25514  nn0prpw  25650  ntruni  25656  clsint2  25658  fnessref  25704  fnemeet2  25727  fnejoin2  25729  filbcmb  25843  mettrifi  25884  heiborlem8  25953  heiborlem10  25955  heibor  25956  riscer  26030  igenval2  26102  oddcomabszz  26440  jm2.19lem4  26496  fiuneneq  26924  idomsubgmo  26925  addrcom  27091  stoweidlem26  27186  stoweidlem34  27194  logccne0  27536  int3  27664  suctrALTcf  27978  suctrALT3  27980  suctrALT4  27984  bnj605  28218  bnj607  28227  bnj964  28254  bnj1033  28278  bnj1128  28299  bnj1137  28304  bnj1136  28306  bnj1413  28344  bnj60  28371  lshpcmp  28457  eqlkr  28568  lkrlsp2  28572  lkrshp  28574  cvrnbtwn2  28744  cvlexch3  28801  cvlexch4N  28802  cvlatexchb1  28803  cvlsupr3  28813  exatleN  28872  cvratlem  28889  atcvrj2b  28900  cvrat3  28910  cvrat4  28911  athgt  28924  ps-1  28945  ps-2  28946  3atlem5  28955  3at  28958  llnneat  28982  llnmlplnN  29007  lplnneat  29013  lplnnelln  29014  islpln2a  29016  lplnriaN  29018  lplnribN  29019  lplnexllnN  29032  2llnjaN  29034  lvolnle3at  29050  lvolneatN  29056  lvolnelln  29057  lvolnelpln  29058  islvol2aN  29060  dalem62  29202  pmapglb2N  29239  pmapglb2xN  29240  lncmp  29251  paddasslem14  29301  paddasslem15  29302  pmod2iN  29317  hlmod1i  29324  pclfinclN  29418  osumcllem8N  29431  pexmidlem4N  29441  pl42lem1N  29447  pl42lem4N  29450  lhpexle1  29476  lhpexle2lem  29477  lhpmcvr5N  29495  lhpmcvr6N  29496  ltrneq  29617  trlnidatb  29645  cdleme0ex2N  29692  cdleme27a  29835  cdleme17d3  29964  cdlemeg46gfre  30000  cdleme48gfv1  30004  cdlemeg49lebilem  30007  cdlemf2  30030  cdlemf  30031  cdlemfnid  30032  trlord  30037  cdlemg31c  30167  cdlemg35  30181  trlcone  30196  tendoeq2  30242  cdlemj3  30291  cdlemk26b-3  30373  cdlemk33N  30377  cdleml3N  30446  cdlemn  30681  dih1dimb2  30710  dihord5apre  30731  dihmeetlem1N  30759  dihglblem5apreN  30760  dihglblem2N  30763  dihglblem3N  30764  dihmeetlem13N  30788  dihmeetlem15N  30790  dihatexv  30807  hdmap14lem12  31351
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