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

Theorem 3expia 1207
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 1204 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 430 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:  mp3an3  1349  3gencl  3110  moi  3251  disji  4405  3optocl  4925  sossfld  5295  f1oresrab  6062  soisores  6225  isomin  6235  isofrlem  6238  ovmpt2s  6426  ov2gf  6427  ndmovord  6465  nnsuc  6715  poxp  6911  brtpos  6982  dfsmo2  7066  smoiun  7080  smoord  7084  smogt  7086  omeulem1  7283  omeu  7286  oewordi  7292  uniinqs  7443  mapvalg  7482  pmvalg  7483  elmapg  7485  xpdom3  7668  mapdom3  7742  php3  7756  unxpdomlem3  7776  isinf  7783  findcard2  7809  isfinite2  7827  ordiso  8029  cnfcom3clem  8207  r111  8243  tskwe  8381  pr2ne  8433  infxpenlem  8441  dfac8alem  8456  infdif  8635  infdif2  8636  cff1  8684  coflim  8687  cfslbn  8693  cfslb2n  8694  cofsmo  8695  cfsmolem  8696  cfcoflem  8698  fin23lem27  8754  isf32lem9  8787  isf34lem6  8806  axcc2lem  8862  domtriomlem  8868  axdc4lem  8881  zorn2lem2  8923  axdclem2  8946  konigthlem  8989  gchen1  9046  gchen2  9047  gchpwdom  9091  gchaleph  9092  winainflem  9114  tskcard  9202  gruiun  9220  gruen  9233  intgru  9235  grudomon  9238  grur1a  9240  grutsk1  9242  nqereu  9350  nqereq  9356  ltsonq  9390  prlem934  9454  reclem3pr  9470  1re  9638  axsup  9705  ltlen  9731  addid2  9812  recex  10240  lemul1a  10455  lt2msq  10487  fimaxre2  10548  zdiv  11002  zextlt  11006  prime  11012  uzind2  11024  fzind  11029  lbzbi  11248  qbtwnxr  11489  qextltlem  11491  xralrple  11494  xltneg  11506  xlt2add  11542  supxrgtmnf  11611  ixxub  11652  ixxlb  11653  ixxlbOLD  11654  ioo0  11657  ico0  11678  ioc0  11679  icc0  11680  iocssre  11710  icossre  11711  iccssre  11712  fzen  11810  expclzlem  12289  expaddz  12309  expmulz  12311  hashgadd  12549  elovmpt2wrd  12692  ccatopth2  12808  shftuz  13111  cau3lem  13396  caubnd  13400  climuni  13594  lo1resb  13606  o1resb  13608  o1of2  13654  o1add  13655  o1mul  13656  o1sub  13657  ntrivcvgmul  13936  eflt  14149  znnenlem  14242  moddvds  14290  dvdscmulr  14309  dvdsmulcr  14310  dvdsle  14328  divalglem8  14358  divalgb  14363  ndvdssub  14366  bitsfzo  14387  gcdcllem1  14451  gcdcllem3  14453  dvdsgcd  14489  lcmgcdlem  14549  lcmfeq0b  14581  isprm3  14611  coprm  14635  qredeu  14642  prmdvdsexpr  14647  prmexpb  14648  eulerthlem2  14708  fermltl  14710  coprimeprodsq  14737  pythagtrip  14762  pcprendvds  14768  pcpremul  14771  pcdvdsb  14796  pc2dvds  14806  4sqlem12  14878  4sqlem18OLD  14884  4sqlem18  14890  vdwlem10  14918  cshwshashlem3  15046  xpslem  15457  ismred  15486  mrieqv2d  15523  iscatd  15557  isfuncd  15748  fthestrcsetc  16013  fthsetcestrc  16028  poslubd  16372  dirtr  16460  ghmrn  16874  pmtrprfv3  17073  mndodcongi  17170  oddvdsnn0  17171  oddvds  17174  odcl2  17194  odhash3  17203  gexdvds  17213  pgpfi  17235  lsmss1b  17295  lsmss2b  17297  efgsrel  17362  efgred  17376  cntzcmn  17458  cyggenod  17497  lt6abl  17507  gsumcom2  17585  pgpfac1lem2  17686  pgpfac1lem3  17688  dvdsunit  17869  unitmulclb  17871  irredrmul  17913  isabvd  18026  lmodvsdi  18092  lss0cl  18148  islbs3  18356  lbsextlem2  18360  mvrf1  18627  coe1fzgsumd  18874  gsummoncoe1  18876  evl1gsumd  18923  xrsdsreclblem  18992  scmataddcl  19518  scmatsubcl  19519  mdetunilem9  19622  mdetuni0  19623  mdetmul  19625  m2cpmrngiso  19759  pm2mpf1  19800  opnnei  20113  neindisj2  20116  cncls2  20266  cncls  20267  cnntr  20268  cnpresti  20281  cnprest  20282  lmcnp  20297  isreg2  20370  ordthauslem  20376  uncon  20421  2ndc1stc  20443  kgen2ss  20547  ptclsg  20607  cnmptcom  20670  kqfvima  20722  hmeof1o  20756  fbncp  20831  fbfinnfr  20833  trfbas2  20835  isufil2  20900  ufprim  20901  trufil  20902  filufint  20912  hausflim  20973  flimrest  20975  flimcls  20977  cnpfcf  21033  alexsubALT  21043  tmdgsum  21087  opnsubg  21099  cldsubg  21102  qustgpopn  21111  tsmsxp  21146  blpnf  21389  blssps  21416  blss  21417  blssec  21427  neibl  21493  prdsxmslem2  21521  xrsmopn  21807  metnrm  21871  climcncf  21909  iccpnfhmeo  21950  xrhmeo  21951  bndth  21963  cphsqrtcl3  22142  iscau2  22224  iscmet3lem2  22239  bcthlem5  22273  bcth3  22276  ishl2  22314  ivthlem1  22379  cmmbl  22465  iundisj2  22479  voliunlem2  22481  mbfaddlem  22593  itg2itg1  22671  itg2seq  22677  itg2mulclem  22681  cnplimc  22819  dvres2  22844  deg1nn0clb  23016  deg1lt0  23017  deg1ge  23024  plypf1  23143  plyadd  23148  plymul  23149  coeeu  23156  dgrub2  23166  coeidlem  23168  coeid3  23171  coemullem  23181  coe11  23184  coemulhi  23185  coemulc  23186  dgreq0  23196  dgrlt  23197  dgradd2  23199  vieta1lem2  23241  sineq0  23453  tanord1  23463  tanord  23464  logccne0  23505  cxpeq0  23600  cxpmul2z  23613  cxpcn3lem  23664  relogbzcl  23688  angpieqvd  23734  o1cxp  23877  scvxcvx  23888  chtublem  24116  bposlem3  24191  lgsqr  24251  dchrisumlema  24303  dchrisumlem2  24305  ostth2lem3  24450  iscgrglt  24536  tghilberti2  24660  inagswap  24857  f1otrg  24878  brbtwn2  24912  axpasch  24948  axcontlem4  24974  axcontlem5  24975  sizeusglecusg  25190  wwlkextproplem3  25447  lpni  25887  gxnn0neg  25967  gxnn0suc  25968  gxcl  25969  gxneg  25970  gxcom  25973  gxinv  25974  gxsuc  25976  gxnn0add  25978  gxadd  25979  gxnn0mul  25981  gxmul  25982  ipasslem5  26452  htthlem  26546  omlsii  27032  spansni  27186  spansneleq  27199  elspansn4  27202  sumspansn  27278  homco1  27430  homulass  27431  mdsl0  27939  ssdmd1  27942  ssdmd2  27943  cvdmd  27966  chirredlem2  28020  atdmd  28027  atmd2  28029  disjif  28168  iundisj2f  28180  isoun  28263  padct  28292  iocinioc2  28346  iundisj2fi  28358  archiabllem1a  28496  archiabllem2a  28499  slmdvsdi  28519  ordtconlem1  28719  indpi1  28832  measinblem  29031  measres  29033  measdivcstOLD  29035  mbfmco2  29076  orvclteinc  29297  sgn3da  29401  sgnnbi  29405  sgnpbi  29406  bnj605  29707  bnj607  29716  bnj964  29743  bnj1033  29767  bnj1128  29788  bnj1137  29793  bnj1136  29795  bnj1413  29833  bnj60  29860  cvmlift2lem10  30024  msubvrs  30187  ghomf1olem  30301  wsuclem  30496  nodense  30564  dfrdg4  30704  brcolinear2  30811  brsegle2  30862  nn0prpw  30965  ntruni  30969  clsint2  30971  fnessref  30999  fnemeet2  31009  fnejoin2  31011  limsucncmpi  31091  ee7.2aOLD  31107  dissneqlem  31677  isbasisrelowllem1  31693  isbasisrelowllem2  31694  icoreclin  31695  poimirlem9  31857  poimirlem30  31878  poimirlem32  31880  areacirc  31945  filbcmb  31975  mettrifi  31994  heiborlem8  32058  heiborlem10  32060  heibor  32061  riscer  32135  igenval2  32207  lshpcmp  32467  eqlkr  32578  lkrlsp2  32582  lkrshp  32584  cvrnbtwn2  32754  cvlexch3  32811  cvlexch4N  32812  cvlatexchb1  32813  cvlsupr3  32823  exatleN  32882  cvratlem  32899  atcvrj2b  32910  cvrat3  32920  cvrat4  32921  athgt  32934  ps-1  32955  ps-2  32956  3atlem5  32965  3at  32968  llnneat  32992  llnmlplnN  33017  lplnneat  33023  lplnnelln  33024  islpln2a  33026  lplnriaN  33028  lplnribN  33029  lplnexllnN  33042  2llnjaN  33044  lvolnle3at  33060  lvolneatN  33066  lvolnelln  33067  lvolnelpln  33068  islvol2aN  33070  dalem62  33212  pmapglb2N  33249  pmapglb2xN  33250  lncmp  33261  paddasslem14  33311  paddasslem15  33312  pmod2iN  33327  hlmod1i  33334  pclfinclN  33428  osumcllem8N  33441  pexmidlem4N  33451  pl42lem1N  33457  pl42lem4N  33460  lhpexle1  33486  lhpexle2lem  33487  lhpmcvr5N  33505  lhpmcvr6N  33506  ltrneq  33627  trlnidatb  33656  cdleme0ex2N  33703  cdleme27a  33847  cdleme17d3  33976  cdlemeg46gfre  34012  cdleme48gfv1  34016  cdlemeg49lebilem  34019  cdlemf2  34042  cdlemf  34043  cdlemfnid  34044  trlord  34049  cdlemg31c  34179  cdlemg35  34193  trlcone  34208  tendoeq2  34254  cdlemj3  34303  cdlemk26b-3  34385  cdlemk33N  34389  cdleml3N  34458  cdlemn  34693  dih1dimb2  34722  dihord5apre  34743  dihmeetlem1N  34771  dihglblem5apreN  34772  dihglblem2N  34775  dihglblem3N  34776  dihmeetlem13N  34800  dihmeetlem15N  34802  dihatexv  34819  hdmap14lem12  35363  oddcomabszz  35706  jm2.19lem4  35761  fiuneneq  35985  idomsubgmo  35986  pwinfi3  36081  binomcxplemnn0  36550  addrcom  36680  int3  36844  suctrALT  37077  suctrALTcf  37174  suctrALT3  37176  chordthmALT  37185  iunconlem2  37187  stoweidlem26  37673  stoweidlem34  37682  nnsgrp  38879  ply1mulgsumlem1  39242
  Copyright terms: Public domain W3C validator