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

Theorem 3expia 1209
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 1206 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp 431 1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 984
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 189  df-an 373  df-3an 986
This theorem is referenced by:  mp3an3  1352  3gencl  3078  moi  3220  disji  4389  3optocl  4912  sossfld  5282  f1oresrab  6053  soisores  6216  isomin  6226  isofrlem  6229  ovmpt2s  6417  ov2gf  6418  ndmovord  6456  nnsuc  6706  poxp  6905  brtpos  6979  dfsmo2  7063  smoiun  7077  smoord  7081  smogt  7083  omeulem1  7280  omeu  7283  oewordi  7289  uniinqs  7440  mapvalg  7479  pmvalg  7480  elmapg  7482  xpdom3  7667  mapdom3  7741  php3  7755  unxpdomlem3  7775  isinf  7782  findcard2  7808  isfinite2  7826  ordiso  8028  cnfcom3clem  8207  r111  8243  tskwe  8381  pr2ne  8433  infxpenlem  8441  dfac8alem  8457  infdif  8636  infdif2  8637  cff1  8685  coflim  8688  cfslbn  8694  cfslb2n  8695  cofsmo  8696  cfsmolem  8697  cfcoflem  8699  fin23lem27  8755  isf32lem9  8788  isf34lem6  8807  axcc2lem  8863  domtriomlem  8869  axdc4lem  8882  zorn2lem2  8924  axdclem2  8947  konigthlem  8990  gchen1  9047  gchen2  9048  gchpwdom  9092  gchaleph  9093  winainflem  9115  tskcard  9203  gruiun  9221  gruen  9234  intgru  9236  grudomon  9239  grur1a  9241  grutsk1  9243  nqereu  9351  nqereq  9357  ltsonq  9391  prlem934  9455  reclem3pr  9471  1re  9639  axsup  9706  ltlen  9732  addid2  9813  recex  10241  lemul1a  10456  lt2msq  10488  fimaxre2  10549  zdiv  11003  zextlt  11007  prime  11013  uzind2  11025  fzind  11030  lbzbi  11249  qbtwnxr  11490  qextltlem  11492  xralrple  11495  xltneg  11507  xlt2add  11543  supxrgtmnf  11612  ixxub  11653  ixxlb  11654  ixxlbOLD  11655  ioo0  11658  ico0  11679  ioc0  11680  icc0  11681  iocssre  11711  icossre  11712  iccssre  11713  fzen  11813  expclzlem  12293  expaddz  12313  expmulz  12315  hashgadd  12553  elovmpt2wrd  12706  ccatopth2  12822  shftuz  13125  cau3lem  13410  caubnd  13414  climuni  13609  lo1resb  13621  o1resb  13623  o1of2  13669  o1add  13670  o1mul  13671  o1sub  13672  ntrivcvgmul  13951  eflt  14164  znnenlem  14257  moddvds  14305  dvdscmulr  14324  dvdsmulcr  14325  dvdsle  14343  divalglem8  14373  divalgb  14378  ndvdssub  14381  bitsfzo  14402  gcdcllem1  14466  gcdcllem3  14468  dvdsgcd  14504  lcmgcdlem  14564  lcmfeq0b  14596  isprm3  14626  coprm  14650  qredeu  14657  prmdvdsexpr  14662  prmexpb  14663  eulerthlem2  14723  fermltl  14725  coprimeprodsq  14752  pythagtrip  14777  pcprendvds  14783  pcpremul  14786  pcdvdsb  14811  pc2dvds  14821  4sqlem12  14893  4sqlem18OLD  14899  4sqlem18  14905  vdwlem10  14933  cshwshashlem3  15061  xpslem  15472  ismred  15501  mrieqv2d  15538  iscatd  15572  isfuncd  15763  fthestrcsetc  16028  fthsetcestrc  16043  poslubd  16387  dirtr  16475  ghmrn  16889  pmtrprfv3  17088  mndodcongi  17185  oddvdsnn0  17186  oddvds  17189  odcl2  17209  odhash3  17218  gexdvds  17228  pgpfi  17250  lsmss1b  17310  lsmss2b  17312  efgsrel  17377  efgred  17391  cntzcmn  17473  cyggenod  17512  lt6abl  17522  gsumcom2  17600  pgpfac1lem2  17701  pgpfac1lem3  17703  dvdsunit  17884  unitmulclb  17886  irredrmul  17928  isabvd  18041  lmodvsdi  18107  lss0cl  18163  islbs3  18371  lbsextlem2  18375  mvrf1  18642  coe1fzgsumd  18889  gsummoncoe1  18891  evl1gsumd  18938  xrsdsreclblem  19007  scmataddcl  19534  scmatsubcl  19535  mdetunilem9  19638  mdetuni0  19639  mdetmul  19641  m2cpmrngiso  19775  pm2mpf1  19816  opnnei  20129  neindisj2  20132  cncls2  20282  cncls  20283  cnntr  20284  cnpresti  20297  cnprest  20298  lmcnp  20313  isreg2  20386  ordthauslem  20392  uncon  20437  2ndc1stc  20459  kgen2ss  20563  ptclsg  20623  cnmptcom  20686  kqfvima  20738  hmeof1o  20772  fbncp  20847  fbfinnfr  20849  trfbas2  20851  isufil2  20916  ufprim  20917  trufil  20918  filufint  20928  hausflim  20989  flimrest  20991  flimcls  20993  cnpfcf  21049  alexsubALT  21059  tmdgsum  21103  opnsubg  21115  cldsubg  21118  qustgpopn  21127  tsmsxp  21162  blpnf  21405  blssps  21432  blss  21433  blssec  21443  neibl  21509  prdsxmslem2  21537  xrsmopn  21823  metnrm  21887  climcncf  21925  iccpnfhmeo  21966  xrhmeo  21967  bndth  21979  cphsqrtcl3  22158  iscau2  22240  iscmet3lem2  22255  bcthlem5  22289  bcth3  22292  ishl2  22330  ivthlem1  22395  cmmbl  22481  iundisj2  22495  voliunlem2  22497  mbfaddlem  22609  itg2itg1  22687  itg2seq  22693  itg2mulclem  22697  cnplimc  22835  dvres2  22860  deg1nn0clb  23032  deg1lt0  23033  deg1ge  23040  plypf1  23159  plyadd  23164  plymul  23165  coeeu  23172  dgrub2  23182  coeidlem  23184  coeid3  23187  coemullem  23197  coe11  23200  coemulhi  23201  coemulc  23202  dgreq0  23212  dgrlt  23213  dgradd2  23215  vieta1lem2  23257  sineq0  23469  tanord1  23479  tanord  23480  logccne0  23521  cxpeq0  23616  cxpmul2z  23629  cxpcn3lem  23680  relogbzcl  23704  angpieqvd  23750  o1cxp  23893  scvxcvx  23904  chtublem  24132  bposlem3  24207  lgsqr  24267  dchrisumlema  24319  dchrisumlem2  24321  ostth2lem3  24466  iscgrglt  24552  tghilberti2  24676  inagswap  24873  f1otrg  24894  brbtwn2  24928  axpasch  24964  axcontlem4  24990  axcontlem5  24991  sizeusglecusg  25207  wwlkextproplem3  25464  lpni  25904  gxnn0neg  25984  gxnn0suc  25985  gxcl  25986  gxneg  25987  gxcom  25990  gxinv  25991  gxsuc  25993  gxnn0add  25995  gxadd  25996  gxnn0mul  25998  gxmul  25999  ipasslem5  26469  htthlem  26563  omlsii  27049  spansni  27203  spansneleq  27216  elspansn4  27219  sumspansn  27295  homco1  27447  homulass  27448  mdsl0  27956  ssdmd1  27959  ssdmd2  27960  cvdmd  27983  chirredlem2  28037  atdmd  28044  atmd2  28046  disjif  28181  iundisj2f  28193  isoun  28275  padct  28300  iocinioc2  28354  iundisj2fi  28366  archiabllem1a  28501  archiabllem2a  28504  slmdvsdi  28524  ordtconlem1  28723  indpi1  28836  measinblem  29035  measres  29037  measdivcstOLD  29039  mbfmco2  29080  orvclteinc  29301  sgn3da  29405  sgnnbi  29409  sgnpbi  29410  bnj605  29711  bnj607  29720  bnj964  29747  bnj1033  29771  bnj1128  29792  bnj1137  29797  bnj1136  29799  bnj1413  29837  bnj60  29864  cvmlift2lem10  30028  msubvrs  30191  ghomf1olem  30305  wsuclem  30501  nosepon  30549  nodense  30571  dfrdg4  30711  brcolinear2  30818  brsegle2  30869  nn0prpw  30972  ntruni  30976  clsint2  30978  fnessref  31006  fnemeet2  31016  fnejoin2  31018  limsucncmpi  31098  ee7.2aOLD  31114  dissneqlem  31735  isbasisrelowllem1  31751  isbasisrelowllem2  31752  icoreclin  31753  poimirlem9  31942  poimirlem30  31963  poimirlem32  31965  areacirc  32030  filbcmb  32060  mettrifi  32079  heiborlem8  32143  heiborlem10  32145  heibor  32146  riscer  32220  igenval2  32292  lshpcmp  32548  eqlkr  32659  lkrlsp2  32663  lkrshp  32665  cvrnbtwn2  32835  cvlexch3  32892  cvlexch4N  32893  cvlatexchb1  32894  cvlsupr3  32904  exatleN  32963  cvratlem  32980  atcvrj2b  32991  cvrat3  33001  cvrat4  33002  athgt  33015  ps-1  33036  ps-2  33037  3atlem5  33046  3at  33049  llnneat  33073  llnmlplnN  33098  lplnneat  33104  lplnnelln  33105  islpln2a  33107  lplnriaN  33109  lplnribN  33110  lplnexllnN  33123  2llnjaN  33125  lvolnle3at  33141  lvolneatN  33147  lvolnelln  33148  lvolnelpln  33149  islvol2aN  33151  dalem62  33293  pmapglb2N  33330  pmapglb2xN  33331  lncmp  33342  paddasslem14  33392  paddasslem15  33393  pmod2iN  33408  hlmod1i  33415  pclfinclN  33509  osumcllem8N  33522  pexmidlem4N  33532  pl42lem1N  33538  pl42lem4N  33541  lhpexle1  33567  lhpexle2lem  33568  lhpmcvr5N  33586  lhpmcvr6N  33587  ltrneq  33708  trlnidatb  33737  cdleme0ex2N  33784  cdleme27a  33928  cdleme17d3  34057  cdlemeg46gfre  34093  cdleme48gfv1  34097  cdlemeg49lebilem  34100  cdlemf2  34123  cdlemf  34124  cdlemfnid  34125  trlord  34130  cdlemg31c  34260  cdlemg35  34274  trlcone  34289  tendoeq2  34335  cdlemj3  34384  cdlemk26b-3  34466  cdlemk33N  34470  cdleml3N  34539  cdlemn  34774  dih1dimb2  34803  dihord5apre  34824  dihmeetlem1N  34852  dihglblem5apreN  34853  dihglblem2N  34856  dihglblem3N  34857  dihmeetlem13N  34881  dihmeetlem15N  34883  dihatexv  34900  hdmap14lem12  35444  oddcomabszz  35786  jm2.19lem4  35841  fiuneneq  36065  idomsubgmo  36066  pwinfi3  36161  binomcxplemnn0  36692  addrcom  36822  int3  36985  suctrALT  37216  suctrALTcf  37313  suctrALT3  37315  chordthmALT  37324  iunconlem2  37326  stoweidlem26  37880  stoweidlem34  37889  upgredg2vtx  39217  usgredg2vtxeuALT  39285  sizusglecusg  39507  vtxduhgr0e  39520  nnsgrp  39804  ply1mulgsumlem1  40165
  Copyright terms: Public domain W3C validator