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 429 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ 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 371  df-3an 976
This theorem is referenced by:  mp3an3  1314  3gencl  3127  moi  3268  disji  4425  reusv6OLD  4648  3optocl  5068  sossfld  5444  f1oresrab  6048  soisores  6208  isomin  6218  isofrlem  6221  ovmpt2s  6411  ov2gf  6412  ndmovord  6450  nnsuc  6702  poxp  6897  brtpos  6966  dfsmo2  7020  smoiun  7034  smoord  7038  smogt  7040  omeulem1  7233  omeu  7236  oewordi  7242  uniinqs  7393  mapvalg  7432  pmvalg  7433  elmapg  7435  xpdom3  7617  mapdom3  7691  php3  7705  unxpdomlem3  7728  isinf  7735  findcard2  7762  isfinite2  7780  ordiso  7944  cnfcom3clem  8152  cnfcom3clemOLD  8160  r111  8196  tskwe  8334  pr2ne  8386  infxpenlem  8394  dfac8alem  8413  infdif  8592  infdif2  8593  cff1  8641  coflim  8644  cfslbn  8650  cfslb2n  8651  cofsmo  8652  cfsmolem  8653  cfcoflem  8655  fin23lem27  8711  isf32lem9  8744  isf34lem6  8763  axcc2lem  8819  domtriomlem  8825  axdc4lem  8838  zorn2lem2  8880  axdclem2  8903  konigthlem  8946  gchen1  9006  gchen2  9007  gchpwdom  9051  gchaleph  9052  winainflem  9074  tskcard  9162  gruiun  9180  gruen  9193  intgru  9195  grudomon  9198  grur1a  9200  grutsk1  9202  nqereu  9310  nqereq  9316  ltsonq  9350  prlem934  9414  reclem3pr  9430  1re  9598  axsup  9663  ltlen  9689  addid2  9766  recex  10188  lemul1a  10403  ledivmulOLD  10426  lt2msq  10436  fimaxre2  10498  zdiv  10940  zextlt  10944  prime  10950  uzind2  10962  fzind  10968  lbzbi  11180  qbtwnxr  11409  qextltlem  11411  xralrple  11414  xltneg  11426  xlt2add  11462  supxrgtmnf  11531  ixxub  11560  ixxlb  11561  ioo0  11564  ico0  11585  ioc0  11586  icc0  11587  iocssre  11614  icossre  11615  iccssre  11616  fzen  11713  expclzlem  12171  expaddz  12191  expmulz  12193  hashgadd  12426  elovmpt2wrd  12564  ccatopth2  12677  shftuz  12883  cau3lem  13168  caubnd  13172  climuni  13356  lo1resb  13368  o1resb  13370  o1of2  13416  o1add  13417  o1mul  13418  o1sub  13419  ntrivcvgmul  13692  eflt  13833  znnenlem  13926  moddvds  13974  dvdscmulr  13993  dvdsmulcr  13994  dvdsle  14012  divalglem8  14039  divalgb  14043  ndvdssub  14046  bitsfzo  14066  gcdcllem1  14130  gcdcllem3  14132  dvdsgcd  14162  isprm3  14207  coprm  14222  qredeu  14229  prmdvdsexpr  14238  prmexpb  14239  eulerthlem2  14293  fermltl  14295  coprimeprodsq  14314  pythagtrip  14339  pcprendvds  14345  pcpremul  14348  pcdvdsb  14373  pc2dvds  14383  4sqlem12  14455  4sqlem18  14461  vdwlem10  14489  cshwshashlem3  14563  xpslem  14951  ismred  14980  mrieqv2d  15017  iscatd  15051  isfuncd  15212  poslubd  15756  dirtr  15844  ghmrn  16258  pmtrprfv3  16457  mndodcongi  16545  oddvdsnn0  16546  oddvds  16549  odcl2  16565  odhash3  16574  gexdvds  16582  pgpfi  16603  lsmss1b  16663  lsmss2b  16665  efgsrel  16730  efgred  16744  cntzcmn  16826  cyggenod  16865  lt6abl  16875  gsumcom2  16981  pgpfac1lem2  17104  pgpfac1lem3  17106  dvdsunit  17290  unitmulclb  17292  irredrmul  17334  isabvd  17447  lmodvsdi  17513  lss0cl  17571  islbs3  17779  lbsextlem2  17783  mvrf1  18059  coe1fzgsumd  18322  gsummoncoe1  18324  evl1gsumd  18371  xrsdsreclblem  18442  scmataddcl  18995  scmatsubcl  18996  mdetunilem9  19099  mdetuni0  19100  mdetmul  19102  m2cpmrngiso  19236  pm2mpf1  19277  opnnei  19598  neindisj2  19601  cncls2  19751  cncls  19752  cnntr  19753  cnpresti  19766  cnprest  19767  lmcnp  19782  isreg2  19855  ordthauslem  19861  uncon  19907  2ndc1stc  19929  kgen2ss  20033  ptclsg  20093  cnmptcom  20156  kqfvima  20208  hmeof1o  20242  fbncp  20317  fbfinnfr  20319  trfbas2  20321  isufil2  20386  ufprim  20387  trufil  20388  filufint  20398  hausflim  20459  flimrest  20461  flimcls  20463  cnpfcf  20519  alexsubALT  20528  tmdgsum  20571  opnsubg  20583  cldsubg  20586  qustgpopn  20595  tsmsxp  20634  blpnf  20877  blssps  20904  blss  20905  blssec  20915  neibl  20981  prdsxmslem2  21009  xrsmopn  21294  metnrm  21343  climcncf  21381  iccpnfhmeo  21422  xrhmeo  21423  bndth  21435  cphsqrtcl3  21611  iscau2  21693  iscmet3lem2  21708  bcthlem5  21744  bcth3  21747  ishl2  21787  ivthlem1  21840  cmmbl  21922  iundisj2  21936  voliunlem2  21938  mbfaddlem  22044  itg2itg1  22120  itg2seq  22126  itg2mulclem  22130  cnplimc  22268  dvres2  22293  deg1nn0clb  22467  deg1lt0  22468  deg1ge  22476  plypf1  22586  plyadd  22591  plymul  22592  coeeu  22599  dgrub2  22609  coeidlem  22611  coeid3  22614  coemullem  22623  coe11  22626  coemulhi  22627  coemulc  22628  dgreq0  22638  dgrlt  22639  dgradd2  22641  vieta1lem2  22683  sineq0  22890  tanord1  22900  tanord  22901  cxpeq0  23035  cxpmul2z  23048  cxpcn3lem  23097  angpieqvd  23138  o1cxp  23280  scvxcvx  23291  chtublem  23462  bposlem3  23537  lgsqr  23597  dchrisumlema  23649  dchrisumlem2  23651  ostth2lem3  23796  tghilbert1_2  23994  f1otrg  24150  brbtwn2  24184  axpasch  24220  axcontlem4  24246  axcontlem5  24247  sizeusglecusg  24462  wwlkextproplem3  24719  lpni  25157  gxnn0neg  25241  gxnn0suc  25242  gxcl  25243  gxneg  25244  gxcom  25247  gxinv  25248  gxsuc  25250  gxnn0add  25252  gxadd  25253  gxnn0mul  25255  gxmul  25256  ipasslem5  25726  htthlem  25810  omlsii  26297  spansni  26451  spansneleq  26464  elspansn4  26467  sumspansn  26543  homco1  26696  homulass  26697  mdsl0  27205  ssdmd1  27208  ssdmd2  27209  cvdmd  27232  chirredlem2  27286  atdmd  27293  atmd2  27295  disjif  27415  iundisj2f  27425  isoun  27496  iocinioc2  27566  iundisj2fi  27578  archiabllem1a  27712  archiabllem2a  27715  slmdvsdi  27735  ordtconlem1  27883  logccne0  27989  indpi1  28012  measinblem  28168  measres  28170  measdivcstOLD  28172  mbfmco2  28213  orvclteinc  28391  sgn3da  28457  sgnnbi  28461  sgnpbi  28462  cvmlift2lem10  28734  msubvrs  28897  ghomf1olem  29011  wsuclem  29356  nodense  29424  dfrdg4  29575  brcolinear2  29683  brsegle2  29734  limsucncmpi  29885  ee7.2aOLD  29901  areacirc  30087  nn0prpw  30116  ntruni  30120  clsint2  30122  fnessref  30150  fnemeet2  30160  fnejoin2  30162  filbcmb  30206  mettrifi  30225  heiborlem8  30289  heiborlem10  30291  heibor  30292  riscer  30366  igenval2  30438  oddcomabszz  30855  jm2.19lem4  30909  fiuneneq  31130  idomsubgmo  31131  lcmgcdlem  31188  addrcom  31338  stoweidlem26  31697  stoweidlem34  31705  nnsgrp  32342  ply1mulgsumlem1  32721  int3  33131  suctrALT  33359  suctrALTcf  33455  suctrALT3  33457  chordthmALT  33466  iunconlem2  33468  bnj605  33698  bnj607  33707  bnj964  33734  bnj1033  33758  bnj1128  33779  bnj1137  33784  bnj1136  33786  bnj1413  33824  bnj60  33851  lshpcmp  34453  eqlkr  34564  lkrlsp2  34568  lkrshp  34570  cvrnbtwn2  34740  cvlexch3  34797  cvlexch4N  34798  cvlatexchb1  34799  cvlsupr3  34809  exatleN  34868  cvratlem  34885  atcvrj2b  34896  cvrat3  34906  cvrat4  34907  athgt  34920  ps-1  34941  ps-2  34942  3atlem5  34951  3at  34954  llnneat  34978  llnmlplnN  35003  lplnneat  35009  lplnnelln  35010  islpln2a  35012  lplnriaN  35014  lplnribN  35015  lplnexllnN  35028  2llnjaN  35030  lvolnle3at  35046  lvolneatN  35052  lvolnelln  35053  lvolnelpln  35054  islvol2aN  35056  dalem62  35198  pmapglb2N  35235  pmapglb2xN  35236  lncmp  35247  paddasslem14  35297  paddasslem15  35298  pmod2iN  35313  hlmod1i  35320  pclfinclN  35414  osumcllem8N  35427  pexmidlem4N  35437  pl42lem1N  35443  pl42lem4N  35446  lhpexle1  35472  lhpexle2lem  35473  lhpmcvr5N  35491  lhpmcvr6N  35492  ltrneq  35613  trlnidatb  35642  cdleme0ex2N  35689  cdleme27a  35833  cdleme17d3  35962  cdlemeg46gfre  35998  cdleme48gfv1  36002  cdlemeg49lebilem  36005  cdlemf2  36028  cdlemf  36029  cdlemfnid  36030  trlord  36035  cdlemg31c  36165  cdlemg35  36179  trlcone  36194  tendoeq2  36240  cdlemj3  36289  cdlemk26b-3  36371  cdlemk33N  36375  cdleml3N  36444  cdlemn  36679  dih1dimb2  36708  dihord5apre  36729  dihmeetlem1N  36757  dihglblem5apreN  36758  dihglblem2N  36761  dihglblem3N  36762  dihmeetlem13N  36786  dihmeetlem15N  36788  dihatexv  36805  hdmap14lem12  37349  pwinfi3  37451
  Copyright terms: Public domain W3C validator