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  2818  moi  2948  disji  4011  reusv6OLD  4545  nnsuc  4673  3optocl  4766  sossfld  5120  soisores  5824  isomin  5834  isofrlem  5837  ovmpt2s  5971  ov2gf  5972  ndmovord  6010  poxp  6227  brtpos  6243  dfsmo2  6364  smoiun  6378  smoord  6382  smogt  6384  omeulem1  6580  omeu  6583  oewordi  6589  mapvalg  6782  pmvalg  6783  elmapg  6785  xpdom3  6960  mapdom3  7033  php3  7047  unxpdomlem3  7069  isinf  7076  findcard2  7098  isfinite2  7115  ordiso  7231  cnfcom3clem  7408  r111  7447  tskwe  7583  pr2ne  7635  infxpenlem  7641  dfac8alem  7656  infdif  7835  infdif2  7836  cff1  7884  coflim  7887  cfslbn  7893  cfslb2n  7894  cofsmo  7895  cfsmolem  7896  cfcoflem  7898  fin23lem27  7954  isf32lem9  7987  isf34lem6  8006  axcc2lem  8062  domtriomlem  8068  axdc4lem  8081  zorn2lem2  8124  axdclem2  8147  konigthlem  8190  gchen1  8247  gchen2  8248  gchpwdom  8296  gchaleph  8297  winainflem  8315  tskcard  8403  gruiun  8421  gruen  8434  intgru  8436  grudomon  8439  grur1a  8441  grutsk1  8443  nqereu  8553  nqereq  8559  ltsonq  8593  prlem934  8657  reclem3pr  8673  1re  8837  axsup  8898  ltlen  8922  addid2  8995  recex  9400  lemul1a  9610  ledivmulOLD  9630  lt2msq  9640  fimaxre2  9702  zdiv  10082  zextlt  10086  prime  10092  uzind2  10104  fzind  10110  lbzbi  10306  qbtwnxr  10527  qextltlem  10529  xralrple  10532  xltneg  10544  xlt2add  10580  supxrgtmnf  10648  ixxub  10677  ixxlb  10678  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  iocssre  10729  icossre  10730  iccssre  10731  fzen  10811  expclzlem  11127  expaddz  11146  expmulz  11148  hashgadd  11359  ccatopth2  11463  shftuz  11564  cau3lem  11838  caubnd  11842  climuni  12026  lo1resb  12038  o1resb  12040  o1of2  12086  o1add  12087  o1mul  12088  o1sub  12089  eflt  12397  znnenlem  12490  moddvds  12538  dvdscmulr  12557  dvdsmulcr  12558  dvdsle  12574  divalglem8  12599  divalgb  12603  ndvdssub  12606  bitsfzo  12626  gcdcllem1  12690  gcdcllem3  12692  dvdsgcd  12722  isprm3  12767  coprm  12779  qredeu  12786  prmdvdsexpr  12795  prmexpb  12796  eulerthlem2  12850  fermltl  12852  coprimeprodsq  12862  pythagtrip  12887  pcprendvds  12893  pcpremul  12896  pcdvdsb  12921  pc2dvds  12931  4sqlem12  13003  4sqlem18  13009  vdwlem10  13037  xpslem  13475  ismred  13504  mrieqv2d  13541  iscatd  13575  isfuncd  13739  poslubd  14251  dirtr  14358  ghmrn  14696  mndodcongi  14858  oddvdsnn0  14859  oddvds  14862  odcl2  14878  odhash3  14887  gexdvds  14895  pgpfi  14916  lsmss1b  14976  lsmss2b  14978  efgsrel  15043  efgred  15057  cntzcmn  15136  cyggenod  15171  lt6abl  15181  gsumcom2  15226  pgpfac1lem2  15310  pgpfac1lem3  15312  dvdsunit  15445  unitmulclb  15447  irredrmul  15489  isabvd  15585  lmodvsdi  15650  lss0cl  15704  islbs3  15908  lbsextlem2  15912  mvrf1  16170  xrsdsreclblem  16417  opnnei  16857  neindisj2  16860  cncls2  17002  cncls  17003  cnntr  17004  cnpresti  17016  cnprest  17017  lmcnp  17032  isreg2  17105  ordthauslem  17111  uncon  17155  2ndc1stc  17177  kgen2ss  17250  ptclsg  17309  cnmptcom  17372  kqfvima  17421  hmeof1o  17455  fbncp  17534  fbfinnfr  17536  trfbas2  17538  isufil2  17603  ufprim  17604  trufil  17605  filufint  17615  hausflim  17676  flimrest  17678  flimcls  17680  cnpfcf  17736  alexsubALT  17745  tmdgsum  17778  opnsubg  17790  cldsubg  17793  divstgpopn  17802  tsmsxp  17837  blpnf  17954  blss  17972  blssec  17981  neibl  18047  prdsxmslem2  18075  xrsmopn  18318  metnrm  18366  climcncf  18404  iccpnfhmeo  18443  xrhmeo  18444  bndth  18456  cphsqrcl3  18623  iscau2  18703  iscmet3lem2  18718  bcthlem5  18750  bcth3  18753  ishl2  18787  ivthlem1  18811  cmmbl  18892  iundisj2  18906  voliunlem2  18908  mbfaddlem  19015  itg2itg1  19091  itg2seq  19097  itg2mulclem  19101  cnplimc  19237  dvres2  19262  deg1nn0clb  19476  deg1lt0  19477  deg1ge  19484  plypf1  19594  plyadd  19599  plymul  19600  coeeu  19607  dgrub2  19617  coeidlem  19619  coeid3  19622  coemullem  19631  coe11  19634  coemulhi  19635  coemulc  19636  dgreq0  19646  dgrlt  19647  dgradd2  19649  vieta1lem2  19691  sineq0  19889  tanord1  19899  tanord  19900  cxpeq0  20025  cxpmul2z  20038  cxpcn3lem  20087  angpieqvd  20128  o1cxp  20269  scvxcvx  20280  chtublem  20450  bposlem3  20525  lgsqr  20585  dchrisumlema  20637  dchrisumlem2  20639  ostth2lem3  20784  lpni  20846  gxnn0neg  20930  gxnn0suc  20931  gxcl  20932  gxneg  20933  gxcom  20936  gxinv  20937  gxsuc  20939  gxnn0add  20941  gxadd  20942  gxnn0mul  20944  gxmul  20945  ipasslem5  21413  htthlem  21497  omlsii  21982  spansni  22136  spansneleq  22149  elspansn4  22152  sumspansn  22228  homco1  22381  homulass  22382  mdsl0  22890  ssdmd1  22893  ssdmd2  22894  cvdmd  22917  chirredlem2  22971  atdmd  22978  atmd2  22980  isoun  23242  iocinioc2  23272  disjif  23355  disjif2  23358  iundisj2fi  23364  iundisj2f  23366  logccne0  23397  measinblem  23547  measres  23549  measdivcstOLD  23551  measdivcst  23552  mbfmco2  23570  indpi1  23605  orvclteinc  23676  cvmlift2lem10  23843  ghomf1olem  24001  nodense  24343  dfrdg4  24488  brbtwn2  24533  axpasch  24569  axcontlem4  24595  axcontlem5  24596  brcolinear2  24681  brsegle2  24732  limsucncmpi  24884  ee7.2aOLD  24900  areacirc  24931  rspc2edv  24963  uninqs  25039  domintreflemb  25062  injsurinj  25149  repcpwti  25161  cbcpcp  25162  prl1  25168  oriso  25214  ubos  25256  curgrpact  25372  ltrran2  25403  ltrooo  25404  fldi  25427  svli2  25484  elioo1t3  25502  intopcoaconb  25540  limptlimpr2lem2  25575  islimrs4  25582  lvsovso  25626  negveud  25668  negveudr  25669  clsmulrv  25683  intvconlem1  25703  cmpassoh  25801  issrc  25867  clscnc  26010  isconcl6a  26103  nn0prpw  26239  ntruni  26245  clsint2  26247  fnessref  26293  fnemeet2  26316  fnejoin2  26318  filbcmb  26432  mettrifi  26473  heiborlem8  26542  heiborlem10  26544  heibor  26545  riscer  26619  igenval2  26691  oddcomabszz  27029  jm2.19lem4  27085  fiuneneq  27513  idomsubgmo  27514  addrcom  27680  stoweidlem26  27775  stoweidlem34  27783  int3  28384  suctrALTcf  28698  suctrALT3  28700  suctrALT4  28704  chordthmALT  28710  bnj605  28939  bnj607  28948  bnj964  28975  bnj1033  28999  bnj1128  29020  bnj1137  29025  bnj1136  29027  bnj1413  29065  bnj60  29092  lshpcmp  29178  eqlkr  29289  lkrlsp2  29293  lkrshp  29295  cvrnbtwn2  29465  cvlexch3  29522  cvlexch4N  29523  cvlatexchb1  29524  cvlsupr3  29534  exatleN  29593  cvratlem  29610  atcvrj2b  29621  cvrat3  29631  cvrat4  29632  athgt  29645  ps-1  29666  ps-2  29667  3atlem5  29676  3at  29679  llnneat  29703  llnmlplnN  29728  lplnneat  29734  lplnnelln  29735  islpln2a  29737  lplnriaN  29739  lplnribN  29740  lplnexllnN  29753  2llnjaN  29755  lvolnle3at  29771  lvolneatN  29777  lvolnelln  29778  lvolnelpln  29779  islvol2aN  29781  dalem62  29923  pmapglb2N  29960  pmapglb2xN  29961  lncmp  29972  paddasslem14  30022  paddasslem15  30023  pmod2iN  30038  hlmod1i  30045  pclfinclN  30139  osumcllem8N  30152  pexmidlem4N  30162  pl42lem1N  30168  pl42lem4N  30171  lhpexle1  30197  lhpexle2lem  30198  lhpmcvr5N  30216  lhpmcvr6N  30217  ltrneq  30338  trlnidatb  30366  cdleme0ex2N  30413  cdleme27a  30556  cdleme17d3  30685  cdlemeg46gfre  30721  cdleme48gfv1  30725  cdlemeg49lebilem  30728  cdlemf2  30751  cdlemf  30752  cdlemfnid  30753  trlord  30758  cdlemg31c  30888  cdlemg35  30902  trlcone  30917  tendoeq2  30963  cdlemj3  31012  cdlemk26b-3  31094  cdlemk33N  31098  cdleml3N  31167  cdlemn  31402  dih1dimb2  31431  dihord5apre  31452  dihmeetlem1N  31480  dihglblem5apreN  31481  dihglblem2N  31484  dihglblem3N  31485  dihmeetlem13N  31509  dihmeetlem15N  31511  dihatexv  31528  hdmap14lem12  32072
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