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

Theorem 3expia 1198
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 1195 . 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 973
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 975
This theorem is referenced by:  mp3an3  1313  3gencl  3145  moi  3286  disji  4435  reusv6OLD  4658  3optocl  5078  sossfld  5454  f1oresrab  6053  soisores  6211  isomin  6221  isofrlem  6224  ovmpt2s  6410  ov2gf  6411  ndmovord  6449  nnsuc  6701  poxp  6895  brtpos  6964  dfsmo2  7018  smoiun  7032  smoord  7036  smogt  7038  omeulem1  7231  omeu  7234  oewordi  7240  uniinqs  7391  mapvalg  7430  pmvalg  7431  elmapg  7433  xpdom3  7615  mapdom3  7689  php3  7703  unxpdomlem3  7726  isinf  7733  findcard2  7760  isfinite2  7778  ordiso  7941  cnfcom3clem  8149  cnfcom3clemOLD  8157  r111  8193  tskwe  8331  pr2ne  8383  infxpenlem  8391  dfac8alem  8410  infdif  8589  infdif2  8590  cff1  8638  coflim  8641  cfslbn  8647  cfslb2n  8648  cofsmo  8649  cfsmolem  8650  cfcoflem  8652  fin23lem27  8708  isf32lem9  8741  isf34lem6  8760  axcc2lem  8816  domtriomlem  8822  axdc4lem  8835  zorn2lem2  8877  axdclem2  8900  konigthlem  8943  gchen1  9003  gchen2  9004  gchpwdom  9048  gchaleph  9049  winainflem  9071  tskcard  9159  gruiun  9177  gruen  9190  intgru  9192  grudomon  9195  grur1a  9197  grutsk1  9199  nqereu  9307  nqereq  9313  ltsonq  9347  prlem934  9411  reclem3pr  9427  1re  9595  axsup  9660  ltlen  9686  addid2  9762  recex  10181  lemul1a  10396  ledivmulOLD  10419  lt2msq  10429  fimaxre2  10491  zdiv  10931  zextlt  10935  prime  10941  uzind2  10953  fzind  10959  lbzbi  11170  qbtwnxr  11399  qextltlem  11401  xralrple  11404  xltneg  11416  xlt2add  11452  supxrgtmnf  11521  ixxub  11550  ixxlb  11551  ioo0  11554  ico0  11575  ioc0  11576  icc0  11577  iocssre  11604  icossre  11605  iccssre  11606  fzen  11703  expclzlem  12158  expaddz  12178  expmulz  12180  hashgadd  12413  elovmpt2wrd  12548  ccatopth2  12659  shftuz  12865  cau3lem  13150  caubnd  13154  climuni  13338  lo1resb  13350  o1resb  13352  o1of2  13398  o1add  13399  o1mul  13400  o1sub  13401  eflt  13713  znnenlem  13806  moddvds  13854  dvdscmulr  13873  dvdsmulcr  13874  dvdsle  13890  divalglem8  13917  divalgb  13921  ndvdssub  13924  bitsfzo  13944  gcdcllem1  14008  gcdcllem3  14010  dvdsgcd  14040  isprm3  14085  coprm  14100  qredeu  14107  prmdvdsexpr  14116  prmexpb  14117  eulerthlem2  14171  fermltl  14173  coprimeprodsq  14192  pythagtrip  14217  pcprendvds  14223  pcpremul  14226  pcdvdsb  14251  pc2dvds  14261  4sqlem12  14333  4sqlem18  14339  vdwlem10  14367  cshwshashlem3  14440  xpslem  14828  ismred  14857  mrieqv2d  14894  iscatd  14928  isfuncd  15092  poslubd  15635  dirtr  15723  ghmrn  16085  pmtrprfv3  16285  mndodcongi  16373  oddvdsnn0  16374  oddvds  16377  odcl2  16393  odhash3  16402  gexdvds  16410  pgpfi  16431  lsmss1b  16491  lsmss2b  16493  efgsrel  16558  efgred  16572  cntzcmn  16651  cyggenod  16690  lt6abl  16700  gsumcom2  16806  pgpfac1lem2  16928  pgpfac1lem3  16930  dvdsunit  17113  unitmulclb  17115  irredrmul  17157  isabvd  17269  lmodvsdi  17335  lss0cl  17393  islbs3  17601  lbsextlem2  17605  mvrf1  17880  coe1fzgsumd  18143  gsummoncoe1  18145  evl1gsumd  18192  xrsdsreclblem  18260  scmataddcl  18813  scmatsubcl  18814  mdetunilem9  18917  mdetuni0  18918  mdetmul  18920  m2cpmrngiso  19054  pm2mpf1  19095  opnnei  19415  neindisj2  19418  cncls2  19568  cncls  19569  cnntr  19570  cnpresti  19583  cnprest  19584  lmcnp  19599  isreg2  19672  ordthauslem  19678  uncon  19724  2ndc1stc  19746  kgen2ss  19819  ptclsg  19879  cnmptcom  19942  kqfvima  19994  hmeof1o  20028  fbncp  20103  fbfinnfr  20105  trfbas2  20107  isufil2  20172  ufprim  20173  trufil  20174  filufint  20184  hausflim  20245  flimrest  20247  flimcls  20249  cnpfcf  20305  alexsubALT  20314  tmdgsum  20357  opnsubg  20369  cldsubg  20372  divstgpopn  20381  tsmsxp  20420  blpnf  20663  blssps  20690  blss  20691  blssec  20701  neibl  20767  prdsxmslem2  20795  xrsmopn  21080  metnrm  21129  climcncf  21167  iccpnfhmeo  21208  xrhmeo  21209  bndth  21221  cphsqrtcl3  21397  iscau2  21479  iscmet3lem2  21494  bcthlem5  21530  bcth3  21533  ishl2  21573  ivthlem1  21626  cmmbl  21708  iundisj2  21722  voliunlem2  21724  mbfaddlem  21830  itg2itg1  21906  itg2seq  21912  itg2mulclem  21916  cnplimc  22054  dvres2  22079  deg1nn0clb  22253  deg1lt0  22254  deg1ge  22262  plypf1  22372  plyadd  22377  plymul  22378  coeeu  22385  dgrub2  22395  coeidlem  22397  coeid3  22400  coemullem  22409  coe11  22412  coemulhi  22413  coemulc  22414  dgreq0  22424  dgrlt  22425  dgradd2  22427  vieta1lem2  22469  sineq0  22675  tanord1  22685  tanord  22686  cxpeq0  22815  cxpmul2z  22828  cxpcn3lem  22877  angpieqvd  22918  o1cxp  23060  scvxcvx  23071  chtublem  23242  bposlem3  23317  lgsqr  23377  dchrisumlema  23429  dchrisumlem2  23431  ostth2lem3  23576  tghilbert1_2  23760  f1otrg  23878  brbtwn2  23912  axpasch  23948  axcontlem4  23974  axcontlem5  23975  sizeusglecusg  24190  wwlkextproplem3  24447  lpni  24885  gxnn0neg  24969  gxnn0suc  24970  gxcl  24971  gxneg  24972  gxcom  24975  gxinv  24976  gxsuc  24978  gxnn0add  24980  gxadd  24981  gxnn0mul  24983  gxmul  24984  ipasslem5  25454  htthlem  25538  omlsii  26025  spansni  26179  spansneleq  26192  elspansn4  26195  sumspansn  26271  homco1  26424  homulass  26425  mdsl0  26933  ssdmd1  26936  ssdmd2  26937  cvdmd  26960  chirredlem2  27014  atdmd  27021  atmd2  27023  disjif  27140  iundisj2f  27150  isoun  27220  iocinioc2  27286  iundisj2fi  27298  archiabllem2a  27428  slmdvsdi  27448  ordtconlem1  27570  nexple  27673  logccne0  27680  indpi1  27703  measinblem  27859  measres  27861  measdivcstOLD  27863  mbfmco2  27904  orvclteinc  28082  sgn3da  28148  sgnnbi  28152  sgnpbi  28153  cvmlift2lem10  28425  ghomf1olem  28537  ntrivcvgmul  28641  wsuclem  28986  nodense  29054  dfrdg4  29205  brcolinear2  29313  brsegle2  29364  limsucncmpi  29515  ee7.2aOLD  29531  areacirc  29717  nn0prpw  29746  ntruni  29750  clsint2  29752  fnessref  29793  fnemeet2  29816  fnejoin2  29818  filbcmb  29862  mettrifi  29881  heiborlem8  29945  heiborlem10  29947  heibor  29948  riscer  30022  igenval2  30094  oddcomabszz  30512  jm2.19lem4  30566  fiuneneq  30787  idomsubgmo  30788  lcmgcdlem  30840  addrcom  30990  stoweidlem26  31354  stoweidlem34  31362  ply1mulgsumlem1  32085  int3  32496  suctrALT  32724  suctrALTcf  32820  suctrALT3  32822  chordthmALT  32831  iunconlem2  32833  bnj605  33062  bnj607  33071  bnj964  33098  bnj1033  33122  bnj1128  33143  bnj1137  33148  bnj1136  33150  bnj1413  33188  bnj60  33215  lshpcmp  33803  eqlkr  33914  lkrlsp2  33918  lkrshp  33920  cvrnbtwn2  34090  cvlexch3  34147  cvlexch4N  34148  cvlatexchb1  34149  cvlsupr3  34159  exatleN  34218  cvratlem  34235  atcvrj2b  34246  cvrat3  34256  cvrat4  34257  athgt  34270  ps-1  34291  ps-2  34292  3atlem5  34301  3at  34304  llnneat  34328  llnmlplnN  34353  lplnneat  34359  lplnnelln  34360  islpln2a  34362  lplnriaN  34364  lplnribN  34365  lplnexllnN  34378  2llnjaN  34380  lvolnle3at  34396  lvolneatN  34402  lvolnelln  34403  lvolnelpln  34404  islvol2aN  34406  dalem62  34548  pmapglb2N  34585  pmapglb2xN  34586  lncmp  34597  paddasslem14  34647  paddasslem15  34648  pmod2iN  34663  hlmod1i  34670  pclfinclN  34764  osumcllem8N  34777  pexmidlem4N  34787  pl42lem1N  34793  pl42lem4N  34796  lhpexle1  34822  lhpexle2lem  34823  lhpmcvr5N  34841  lhpmcvr6N  34842  ltrneq  34963  trlnidatb  34991  cdleme0ex2N  35038  cdleme27a  35181  cdleme17d3  35310  cdlemeg46gfre  35346  cdleme48gfv1  35350  cdlemeg49lebilem  35353  cdlemf2  35376  cdlemf  35377  cdlemfnid  35378  trlord  35383  cdlemg31c  35513  cdlemg35  35527  trlcone  35542  tendoeq2  35588  cdlemj3  35637  cdlemk26b-3  35719  cdlemk33N  35723  cdleml3N  35792  cdlemn  36027  dih1dimb2  36056  dihord5apre  36077  dihmeetlem1N  36105  dihglblem5apreN  36106  dihglblem2N  36109  dihglblem3N  36110  dihmeetlem13N  36134  dihmeetlem15N  36136  dihatexv  36153  hdmap14lem12  36697
  Copyright terms: Public domain W3C validator