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

Theorem 3expia 1189
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 1186 . 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 965
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 967
This theorem is referenced by:  mp3an3  1303  3gencl  3025  moi  3163  disji  4301  reusv6OLD  4524  3optocl  4936  sossfld  5306  f1oresrab  5896  soisores  6039  isomin  6049  isofrlem  6052  ovmpt2s  6235  ov2gf  6236  ndmovord  6274  nnsuc  6514  poxp  6705  brtpos  6775  dfsmo2  6829  smoiun  6843  smoord  6847  smogt  6849  omeulem1  7042  omeu  7045  oewordi  7051  uniinqs  7201  mapvalg  7245  pmvalg  7246  elmapg  7248  xpdom3  7430  mapdom3  7504  php3  7518  unxpdomlem3  7540  isinf  7547  findcard2  7573  isfinite2  7591  ordiso  7751  cnfcom3clem  7959  cnfcom3clemOLD  7967  r111  8003  tskwe  8141  pr2ne  8193  infxpenlem  8201  dfac8alem  8220  infdif  8399  infdif2  8400  cff1  8448  coflim  8451  cfslbn  8457  cfslb2n  8458  cofsmo  8459  cfsmolem  8460  cfcoflem  8462  fin23lem27  8518  isf32lem9  8551  isf34lem6  8570  axcc2lem  8626  domtriomlem  8632  axdc4lem  8645  zorn2lem2  8687  axdclem2  8710  konigthlem  8753  gchen1  8813  gchen2  8814  gchpwdom  8858  gchaleph  8859  winainflem  8881  tskcard  8969  gruiun  8987  gruen  9000  intgru  9002  grudomon  9005  grur1a  9007  grutsk1  9009  nqereu  9119  nqereq  9125  ltsonq  9159  prlem934  9223  reclem3pr  9239  1re  9406  axsup  9471  ltlen  9497  addid2  9573  recex  9989  lemul1a  10204  ledivmulOLD  10227  lt2msq  10237  fimaxre2  10299  zdiv  10733  zextlt  10737  prime  10743  uzind2  10755  fzind  10761  lbzbi  10964  qbtwnxr  11191  qextltlem  11193  xralrple  11196  xltneg  11208  xlt2add  11244  supxrgtmnf  11313  ixxub  11342  ixxlb  11343  ioo0  11346  ico0  11367  ioc0  11368  icc0  11369  iocssre  11396  icossre  11397  iccssre  11398  fzen  11488  expclzlem  11910  expaddz  11929  expmulz  11931  hashgadd  12161  ccatopth2  12386  shftuz  12579  cau3lem  12863  caubnd  12867  climuni  13051  lo1resb  13063  o1resb  13065  o1of2  13111  o1add  13112  o1mul  13113  o1sub  13114  eflt  13422  znnenlem  13515  moddvds  13563  dvdscmulr  13582  dvdsmulcr  13583  dvdsle  13599  divalglem8  13625  divalgb  13629  ndvdssub  13632  bitsfzo  13652  gcdcllem1  13716  gcdcllem3  13718  dvdsgcd  13748  isprm3  13793  coprm  13807  qredeu  13814  prmdvdsexpr  13823  prmexpb  13824  eulerthlem2  13878  fermltl  13880  coprimeprodsq  13897  pythagtrip  13922  pcprendvds  13928  pcpremul  13931  pcdvdsb  13956  pc2dvds  13966  4sqlem12  14038  4sqlem18  14044  vdwlem10  14072  cshwshashlem3  14145  xpslem  14532  ismred  14561  mrieqv2d  14598  iscatd  14632  isfuncd  14796  poslubd  15339  dirtr  15427  ghmrn  15781  pmtrprfv3  15981  mndodcongi  16067  oddvdsnn0  16068  oddvds  16071  odcl2  16087  odhash3  16096  gexdvds  16104  pgpfi  16125  lsmss1b  16185  lsmss2b  16187  efgsrel  16252  efgred  16266  cntzcmn  16345  cyggenod  16382  lt6abl  16392  gsumcom2  16489  pgpfac1lem2  16598  pgpfac1lem3  16600  dvdsunit  16777  unitmulclb  16779  irredrmul  16821  isabvd  16927  lmodvsdi  16993  lss0cl  17050  islbs3  17258  lbsextlem2  17262  mvrf1  17520  evl1gsumd  17813  xrsdsreclblem  17881  mdetunilem9  18448  mdetuni0  18449  mdetmul  18451  opnnei  18746  neindisj2  18749  cncls2  18899  cncls  18900  cnntr  18901  cnpresti  18914  cnprest  18915  lmcnp  18930  isreg2  19003  ordthauslem  19009  uncon  19055  2ndc1stc  19077  kgen2ss  19150  ptclsg  19210  cnmptcom  19273  kqfvima  19325  hmeof1o  19359  fbncp  19434  fbfinnfr  19436  trfbas2  19438  isufil2  19503  ufprim  19504  trufil  19505  filufint  19515  hausflim  19576  flimrest  19578  flimcls  19580  cnpfcf  19636  alexsubALT  19645  tmdgsum  19688  opnsubg  19700  cldsubg  19703  divstgpopn  19712  tsmsxp  19751  blpnf  19994  blssps  20021  blss  20022  blssec  20032  neibl  20098  prdsxmslem2  20126  xrsmopn  20411  metnrm  20460  climcncf  20498  iccpnfhmeo  20539  xrhmeo  20540  bndth  20552  cphsqrcl3  20728  iscau2  20810  iscmet3lem2  20825  bcthlem5  20861  bcth3  20864  ishl2  20904  ivthlem1  20957  cmmbl  21038  iundisj2  21052  voliunlem2  21054  mbfaddlem  21160  itg2itg1  21236  itg2seq  21242  itg2mulclem  21246  cnplimc  21384  dvres2  21409  deg1nn0clb  21583  deg1lt0  21584  deg1ge  21592  plypf1  21702  plyadd  21707  plymul  21708  coeeu  21715  dgrub2  21725  coeidlem  21727  coeid3  21730  coemullem  21739  coe11  21742  coemulhi  21743  coemulc  21744  dgreq0  21754  dgrlt  21755  dgradd2  21757  vieta1lem2  21799  sineq0  22005  tanord1  22015  tanord  22016  cxpeq0  22145  cxpmul2z  22158  cxpcn3lem  22207  angpieqvd  22248  o1cxp  22390  scvxcvx  22401  chtublem  22572  bposlem3  22647  lgsqr  22707  dchrisumlema  22759  dchrisumlem2  22761  ostth2lem3  22906  tghilbert1_2  23066  f1otrg  23139  brbtwn2  23173  axpasch  23209  axcontlem4  23235  axcontlem5  23236  sizeusglecusg  23416  lpni  23688  gxnn0neg  23772  gxnn0suc  23773  gxcl  23774  gxneg  23775  gxcom  23778  gxinv  23779  gxsuc  23781  gxnn0add  23783  gxadd  23784  gxnn0mul  23786  gxmul  23787  ipasslem5  24257  htthlem  24341  omlsii  24828  spansni  24982  spansneleq  24995  elspansn4  24998  sumspansn  25074  homco1  25227  homulass  25228  mdsl0  25736  ssdmd1  25739  ssdmd2  25740  cvdmd  25763  chirredlem2  25817  atdmd  25824  atmd2  25826  disjif  25944  iundisj2f  25954  isoun  26019  iocinioc2  26091  iundisj2fi  26103  archiabllem2a  26233  slmdvsdi  26253  ordtconlem1  26376  nexple  26470  logccne0  26477  indpi1  26500  measinblem  26656  measres  26658  measdivcstOLD  26660  mbfmco2  26702  orvclteinc  26880  sgn3da  26946  sgnnbi  26950  sgnpbi  26951  cvmlift2lem10  27223  ghomf1olem  27335  ntrivcvgmul  27439  wsuclem  27784  nodense  27852  dfrdg4  28003  brcolinear2  28111  brsegle2  28162  limsucncmpi  28313  ee7.2aOLD  28329  areacirc  28515  nn0prpw  28544  ntruni  28548  clsint2  28550  fnessref  28591  fnemeet2  28614  fnejoin2  28616  filbcmb  28660  mettrifi  28679  heiborlem8  28743  heiborlem10  28745  heibor  28746  riscer  28820  igenval2  28892  oddcomabszz  29311  jm2.19lem4  29367  fiuneneq  29588  idomsubgmo  29589  addrcom  29757  stoweidlem26  29847  stoweidlem34  29855  elovmpt2wrd  30282  wwlkextproplem3  30588  coe1fzgsumd  30871  gsummoncoe1  30876  ply1mulgsumlem1  30877  mat2cnstpmatrngiso  31105  int3  31430  suctrALT  31658  suctrALTcf  31754  suctrALT3  31756  chordthmALT  31765  iunconlem2  31767  bnj605  31996  bnj607  32005  bnj964  32032  bnj1033  32056  bnj1128  32077  bnj1137  32082  bnj1136  32084  bnj1413  32122  bnj60  32149  lshpcmp  32729  eqlkr  32840  lkrlsp2  32844  lkrshp  32846  cvrnbtwn2  33016  cvlexch3  33073  cvlexch4N  33074  cvlatexchb1  33075  cvlsupr3  33085  exatleN  33144  cvratlem  33161  atcvrj2b  33172  cvrat3  33182  cvrat4  33183  athgt  33196  ps-1  33217  ps-2  33218  3atlem5  33227  3at  33230  llnneat  33254  llnmlplnN  33279  lplnneat  33285  lplnnelln  33286  islpln2a  33288  lplnriaN  33290  lplnribN  33291  lplnexllnN  33304  2llnjaN  33306  lvolnle3at  33322  lvolneatN  33328  lvolnelln  33329  lvolnelpln  33330  islvol2aN  33332  dalem62  33474  pmapglb2N  33511  pmapglb2xN  33512  lncmp  33523  paddasslem14  33573  paddasslem15  33574  pmod2iN  33589  hlmod1i  33596  pclfinclN  33690  osumcllem8N  33703  pexmidlem4N  33713  pl42lem1N  33719  pl42lem4N  33722  lhpexle1  33748  lhpexle2lem  33749  lhpmcvr5N  33767  lhpmcvr6N  33768  ltrneq  33889  trlnidatb  33917  cdleme0ex2N  33964  cdleme27a  34107  cdleme17d3  34236  cdlemeg46gfre  34272  cdleme48gfv1  34276  cdlemeg49lebilem  34279  cdlemf2  34302  cdlemf  34303  cdlemfnid  34304  trlord  34309  cdlemg31c  34439  cdlemg35  34453  trlcone  34468  tendoeq2  34514  cdlemj3  34563  cdlemk26b-3  34645  cdlemk33N  34649  cdleml3N  34718  cdlemn  34953  dih1dimb2  34982  dihord5apre  35003  dihmeetlem1N  35031  dihglblem5apreN  35032  dihglblem2N  35035  dihglblem3N  35036  dihmeetlem13N  35060  dihmeetlem15N  35062  dihatexv  35079  hdmap14lem12  35623
  Copyright terms: Public domain W3C validator