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

Theorem 3expia 1182
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 1179 . 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 958
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 960
This theorem is referenced by:  mp3an3  1296  3gencl  2993  moi  3131  disji  4268  reusv6OLD  4491  3optocl  4902  sossfld  5273  f1oresrab  5862  soisores  6005  isomin  6015  isofrlem  6018  ovmpt2s  6203  ov2gf  6204  ndmovord  6242  nnsuc  6482  poxp  6673  brtpos  6743  dfsmo2  6794  smoiun  6808  smoord  6812  smogt  6814  omeulem1  7009  omeu  7012  oewordi  7018  uniinqs  7168  mapvalg  7212  pmvalg  7213  elmapg  7215  xpdom3  7397  mapdom3  7471  php3  7485  unxpdomlem3  7507  isinf  7514  findcard2  7540  isfinite2  7558  ordiso  7718  cnfcom3clem  7926  cnfcom3clemOLD  7934  r111  7970  tskwe  8108  pr2ne  8160  infxpenlem  8168  dfac8alem  8187  infdif  8366  infdif2  8367  cff1  8415  coflim  8418  cfslbn  8424  cfslb2n  8425  cofsmo  8426  cfsmolem  8427  cfcoflem  8429  fin23lem27  8485  isf32lem9  8518  isf34lem6  8537  axcc2lem  8593  domtriomlem  8599  axdc4lem  8612  zorn2lem2  8654  axdclem2  8677  konigthlem  8720  gchen1  8780  gchen2  8781  gchpwdom  8825  gchaleph  8826  winainflem  8848  tskcard  8936  gruiun  8954  gruen  8967  intgru  8969  grudomon  8972  grur1a  8974  grutsk1  8976  nqereu  9086  nqereq  9092  ltsonq  9126  prlem934  9190  reclem3pr  9206  1re  9373  axsup  9438  ltlen  9464  addid2  9540  recex  9956  lemul1a  10171  ledivmulOLD  10194  lt2msq  10204  fimaxre2  10266  zdiv  10700  zextlt  10704  prime  10710  uzind2  10722  fzind  10728  lbzbi  10931  qbtwnxr  11158  qextltlem  11160  xralrple  11163  xltneg  11175  xlt2add  11211  supxrgtmnf  11280  ixxub  11309  ixxlb  11310  ioo0  11313  ico0  11334  ioc0  11335  icc0  11336  iocssre  11363  icossre  11364  iccssre  11365  fzen  11454  expclzlem  11873  expaddz  11892  expmulz  11894  hashgadd  12124  ccatopth2  12349  shftuz  12542  cau3lem  12826  caubnd  12830  climuni  13014  lo1resb  13026  o1resb  13028  o1of2  13074  o1add  13075  o1mul  13076  o1sub  13077  eflt  13384  znnenlem  13477  moddvds  13525  dvdscmulr  13544  dvdsmulcr  13545  dvdsle  13561  divalglem8  13587  divalgb  13591  ndvdssub  13594  bitsfzo  13614  gcdcllem1  13678  gcdcllem3  13680  dvdsgcd  13710  isprm3  13755  coprm  13769  qredeu  13776  prmdvdsexpr  13785  prmexpb  13786  eulerthlem2  13840  fermltl  13842  coprimeprodsq  13859  pythagtrip  13884  pcprendvds  13890  pcpremul  13893  pcdvdsb  13918  pc2dvds  13928  4sqlem12  14000  4sqlem18  14006  vdwlem10  14034  cshwshashlem3  14107  xpslem  14494  ismred  14523  mrieqv2d  14560  iscatd  14594  isfuncd  14758  poslubd  15301  dirtr  15389  ghmrn  15740  pmtrprfv3  15940  mndodcongi  16026  oddvdsnn0  16027  oddvds  16030  odcl2  16046  odhash3  16055  gexdvds  16063  pgpfi  16084  lsmss1b  16144  lsmss2b  16146  efgsrel  16211  efgred  16225  cntzcmn  16304  cyggenod  16341  lt6abl  16351  gsumcom2  16441  pgpfac1lem2  16550  pgpfac1lem3  16552  dvdsunit  16689  unitmulclb  16691  irredrmul  16733  isabvd  16829  lmodvsdi  16895  lss0cl  16950  islbs3  17158  lbsextlem2  17162  mvrf1  17432  xrsdsreclblem  17703  mdetunilem9  18268  mdetuni0  18269  mdetmul  18271  opnnei  18566  neindisj2  18569  cncls2  18719  cncls  18720  cnntr  18721  cnpresti  18734  cnprest  18735  lmcnp  18750  isreg2  18823  ordthauslem  18829  uncon  18875  2ndc1stc  18897  kgen2ss  18970  ptclsg  19030  cnmptcom  19093  kqfvima  19145  hmeof1o  19179  fbncp  19254  fbfinnfr  19256  trfbas2  19258  isufil2  19323  ufprim  19324  trufil  19325  filufint  19335  hausflim  19396  flimrest  19398  flimcls  19400  cnpfcf  19456  alexsubALT  19465  tmdgsum  19508  opnsubg  19520  cldsubg  19523  divstgpopn  19532  tsmsxp  19571  blpnf  19814  blssps  19841  blss  19842  blssec  19852  neibl  19918  prdsxmslem2  19946  xrsmopn  20231  metnrm  20280  climcncf  20318  iccpnfhmeo  20359  xrhmeo  20360  bndth  20372  cphsqrcl3  20548  iscau2  20630  iscmet3lem2  20645  bcthlem5  20681  bcth3  20684  ishl2  20724  ivthlem1  20777  cmmbl  20858  iundisj2  20872  voliunlem2  20874  mbfaddlem  20980  itg2itg1  21056  itg2seq  21062  itg2mulclem  21066  cnplimc  21204  dvres2  21229  deg1nn0clb  21446  deg1lt0  21447  deg1ge  21455  plypf1  21565  plyadd  21570  plymul  21571  coeeu  21578  dgrub2  21588  coeidlem  21590  coeid3  21593  coemullem  21602  coe11  21605  coemulhi  21606  coemulc  21607  dgreq0  21617  dgrlt  21618  dgradd2  21620  vieta1lem2  21662  sineq0  21868  tanord1  21878  tanord  21879  cxpeq0  22008  cxpmul2z  22021  cxpcn3lem  22070  angpieqvd  22111  o1cxp  22253  scvxcvx  22264  chtublem  22435  bposlem3  22510  lgsqr  22570  dchrisumlema  22622  dchrisumlem2  22624  ostth2lem3  22769  tghilbert1_2  22915  f1otrg  22940  brbtwn2  22974  axpasch  23010  axcontlem4  23036  axcontlem5  23037  sizeusglecusg  23217  lpni  23489  gxnn0neg  23573  gxnn0suc  23574  gxcl  23575  gxneg  23576  gxcom  23579  gxinv  23580  gxsuc  23582  gxnn0add  23584  gxadd  23585  gxnn0mul  23587  gxmul  23588  ipasslem5  24058  htthlem  24142  omlsii  24629  spansni  24783  spansneleq  24796  elspansn4  24799  sumspansn  24875  homco1  25028  homulass  25029  mdsl0  25537  ssdmd1  25540  ssdmd2  25541  cvdmd  25564  chirredlem2  25618  atdmd  25625  atmd2  25627  disjif  25746  iundisj2f  25756  isoun  25821  iocinioc2  25892  iundisj2fi  25904  archiabllem2a  26035  slmdvsdi  26080  ordtconlem1  26208  nexple  26302  logccne0  26309  indpi1  26332  measinblem  26488  measres  26490  measdivcstOLD  26492  mbfmco2  26534  orvclteinc  26706  sgn3da  26772  sgnnbi  26776  sgnpbi  26777  cvmlift2lem10  27049  ghomf1olem  27160  ntrivcvgmul  27264  wsuclem  27609  nodense  27677  dfrdg4  27828  brcolinear2  27936  brsegle2  27987  limsucncmpi  28139  ee7.2aOLD  28155  areacirc  28333  nn0prpw  28362  ntruni  28366  clsint2  28368  fnessref  28409  fnemeet2  28432  fnejoin2  28434  filbcmb  28478  mettrifi  28497  heiborlem8  28561  heiborlem10  28563  heibor  28564  riscer  28638  igenval2  28710  oddcomabszz  29130  jm2.19lem4  29186  fiuneneq  29407  idomsubgmo  29408  addrcom  29576  stoweidlem26  29667  stoweidlem34  29675  elovmpt2wrd  30102  wwlkextproplem3  30408  int3  31036  suctrALT  31264  suctrALTcf  31360  suctrALT3  31362  chordthmALT  31371  iunconlem2  31373  bnj605  31602  bnj607  31611  bnj964  31638  bnj1033  31662  bnj1128  31683  bnj1137  31688  bnj1136  31690  bnj1413  31728  bnj60  31755  lshpcmp  32206  eqlkr  32317  lkrlsp2  32321  lkrshp  32323  cvrnbtwn2  32493  cvlexch3  32550  cvlexch4N  32551  cvlatexchb1  32552  cvlsupr3  32562  exatleN  32621  cvratlem  32638  atcvrj2b  32649  cvrat3  32659  cvrat4  32660  athgt  32673  ps-1  32694  ps-2  32695  3atlem5  32704  3at  32707  llnneat  32731  llnmlplnN  32756  lplnneat  32762  lplnnelln  32763  islpln2a  32765  lplnriaN  32767  lplnribN  32768  lplnexllnN  32781  2llnjaN  32783  lvolnle3at  32799  lvolneatN  32805  lvolnelln  32806  lvolnelpln  32807  islvol2aN  32809  dalem62  32951  pmapglb2N  32988  pmapglb2xN  32989  lncmp  33000  paddasslem14  33050  paddasslem15  33051  pmod2iN  33066  hlmod1i  33073  pclfinclN  33167  osumcllem8N  33180  pexmidlem4N  33190  pl42lem1N  33196  pl42lem4N  33199  lhpexle1  33225  lhpexle2lem  33226  lhpmcvr5N  33244  lhpmcvr6N  33245  ltrneq  33366  trlnidatb  33394  cdleme0ex2N  33441  cdleme27a  33584  cdleme17d3  33713  cdlemeg46gfre  33749  cdleme48gfv1  33753  cdlemeg49lebilem  33756  cdlemf2  33779  cdlemf  33780  cdlemfnid  33781  trlord  33786  cdlemg31c  33916  cdlemg35  33930  trlcone  33945  tendoeq2  33991  cdlemj3  34040  cdlemk26b-3  34122  cdlemk33N  34126  cdleml3N  34195  cdlemn  34430  dih1dimb2  34459  dihord5apre  34480  dihmeetlem1N  34508  dihglblem5apreN  34509  dihglblem2N  34512  dihglblem3N  34513  dihmeetlem13N  34537  dihmeetlem15N  34539  dihatexv  34556  hdmap14lem12  35100
  Copyright terms: Public domain W3C validator