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

Theorem 3adant2 1015
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3adant2  |-  ( (
ph  /\  th  /\  ps )  ->  ch )

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 994 . 2  |-  ( (
ph  /\  th  /\  ps )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 16 1  |-  ( (
ph  /\  th  /\  ps )  ->  ch )
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:  3ad2ant1  1017  eupickb  2366  eupickbOLD  2367  vtoclegft  3185  eqeu  3274  funopg  5618  fnco  5687  dff1o2  5819  fnimapr  5929  fvmptt  5963  fnreseql  5989  f1elima  6157  f13dfv  6166  f1ocnvfvb  6171  oprssov  6426  ordunel  6640  poxp  6892  smoiso  7030  oaord  7193  oaword  7195  omcan  7215  omwordri  7218  odi  7225  omeulem1  7228  oeord  7234  oecan  7235  oewordri  7238  oeordsuc  7240  nnaord  7265  nnaordr  7266  nndi  7269  nnaword  7273  nnmwordri  7282  erov  7405  ecopovtrn  7411  xpdom3  7612  mapxpen  7680  findcard  7755  indexfi  7824  suppr  7925  r111  8189  tcrank  8298  acndom  8428  infdif2  8586  infxpdom  8587  cfeq0  8632  cfsuc  8633  cfflb  8635  cflim2  8639  cfsmolem  8646  axcc3  8814  domtriomlem  8818  axdc3lem2  8827  axdc3lem4  8829  axdc4lem  8831  axcclem  8833  pwcfsdom  8954  tsktrss  9135  tsksuc  9136  tskuni  9157  adderpqlem  9328  mulerpqlem  9329  mulcanenq  9334  distrnq  9335  ltsonq  9343  ltanq  9345  ltmnq  9346  distrlem1pr  9399  distrlem5pr  9401  ltsopr  9406  ltsosr  9467  ltasr  9473  adddir  9583  axlttrn  9653  letr  9674  ltneOLD  9678  nnncan1  9851  npncan3  9853  pnpcan2  9855  subdi  9986  subdir  9987  mulcan1g  10198  mulcan2g  10199  divmul  10206  div23  10222  div13  10224  divsubdir  10236  divcan7  10249  ltmul2  10389  lemul1  10390  lemul2  10391  lemul2a  10393  lediv1  10403  ltmuldiv2  10412  lemuldiv  10420  lemuldiv2  10421  ltdiv2  10426  lediv2  10431  infmrlb  10520  nndivtr  10573  bndndx  10790  nn0n0n1ge2  10855  fnn0ind  10956  lbzbi  11166  xrletr  11357  qsqueeze  11396  xleadd2a  11442  xleadd1  11443  xltadd2  11445  xltmul2  11481  supxrbnd  11516  iooneg  11636  iccneg  11637  icoshft  11638  icoshftf1o  11639  fzen  11699  uzsubsubfz  11703  fzrevral2  11759  fzshftral  11761  fz0fzdiffz0  11777  elfzmlbm  11778  elfzmlbp  11779  elfzo  11795  fzoaddel2  11838  fzosubel2  11840  elfzom1p1elfzo  11859  ssfzo12bi  11871  fzonfzoufzol  11877  flltdivnn0lt  11929  modmulnn  11977  modcyc  11995  modaddabs  11998  modaddmod  11999  modadd2mod  12001  modsubmod  12009  modsubmodmod  12010  modaddmodup  12014  modmulmod  12016  moddi  12018  modsubdir  12019  uzindi  12055  axdc4uzlem  12056  expneg2  12139  expdiv  12180  expubnd  12190  bernneq2  12257  hashinfxadd  12417  brfi1indlem  12493  ccatsymb  12561  ccatfv0  12562  ccats1val2  12590  swrdnd  12616  swrdvalodm2  12623  2swrd1eqwrdeq  12638  swrdswrd  12644  wrd2ind  12662  swrdccatin1  12667  swrdccatin12lem2b  12670  swrdccatin2  12671  swrdccatin12lem2  12673  swrdccatin12lem3  12674  swrdccat  12677  swrdccat3a  12678  swrdccat3blem  12679  repswswrd  12715  repswccat  12716  cshwidxmod  12733  2cshw  12740  3cshw  12745  scshwfzeqfzo  12753  cshwcsh2id  12755  ccatco  12760  cshco  12761  swrdco  12762  lswco  12763  swrds2  12842  2swrd2eqwrdeq  12850  shftuz  12861  shftval2  12867  abs3dif  13123  modfsummods  13566  sin02gt0  13784  dvdsval2  13846  dvdscmul  13867  dvdsmulc  13868  dvdscmulr  13869  dvdsmulcr  13870  mulmoddvds  13899  divalglem8  13913  ndvdssub  13920  rpmulgcd  14048  isprm3  14081  coprmdvds  14098  modprm0  14185  coprimeprodsq  14188  pythagtriplem12  14205  pythagtriplem14  14207  pcprendvds  14219  pcmul  14230  pcdiv  14231  pcqcl  14235  pcqdiv  14236  pcdvdsb  14247  pcgcd  14256  vdwnnlem1  14368  hashbcss  14377  cshwshashlem1  14434  fvsetsid  14511  mrcss  14867  mrcsscl  14871  mrcun  14873  cofulid  15113  catcisolem  15287  latleeqj1  15546  lubun  15606  clatleglb  15609  pslem  15689  dirtr  15719  pwspjmhm  15809  gsumccat  15832  grpinvid1  15899  grpinvid2  15900  grpinvadd  15917  grpsubf  15918  grpsubrcan  15920  grpinvsub  15921  grpsubeq0  15925  grpsubadd0sub  15926  grppncan  15930  grpnpcan  15931  mulgnn0p1  15953  subgsubcl  16007  subgsub  16008  eqglact  16047  divssub  16056  ghmsub  16070  psgnunilem4  16318  oddvds2  16384  odsubdvds  16387  gexnnod  16404  slwn0  16431  gsumdixpOLD  17041  gsumdixp  17042  dvrcl  17119  unitdvcl  17120  dvrcan1  17124  dvrcan3  17125  dvreq1  17126  subrgdv  17229  abvsubtri  17267  idsrngd  17294  lmodvsubval2  17348  lsmcl  17512  lsmsp2  17516  lspsntrim  17527  lidldvgen  17685  evlslem4OLD  17944  evlslem4  17945  mpfsubrg  17972  ply1tmcl  18084  eqcoe1ply1eq  18110  gsummoncoe1  18117  lply1binomsc  18120  chrcong  18333  zndvds  18355  zntoslem  18362  ocvsscon  18473  obselocv  18526  frlmphl  18579  mamudm  18657  mamufacex  18658  scmatf1  18800  scmatf1o  18801  scmatrngiso  18805  submabas  18847  mdetdiaglem  18867  mdetralt2  18878  mdetero  18879  mdetunilem2  18882  mdetunilem6  18886  m2detleiblem7  18896  maducoeval2  18909  gsummatr01lem3  18926  gsummatr01  18928  smadiadetglem2  18941  cramerlem1  18956  mply1topmatcl  19073  mp2pm2mplem4  19077  istps3OLD  19190  ntrin  19328  elnei  19378  neindisj2  19390  ordtopn3  19463  ordtcld3  19466  leordtval2  19479  lecldbas  19486  cnrest2  19553  cmpsublem  19665  ptrescn  19875  xkococn  19896  kqfeq  19960  snfbas  20102  neifil  20116  fclsrest  20260  utopsnnei  20487  neipcfilu  20534  psmetsym  20549  psmetge0  20551  xmetge0  20582  xmetsym  20585  metusttoOLD  20795  metustto  20796  metustblOLD  20818  metustbl  20819  restmetu  20825  nm2dif  20879  nmtri  20880  cnmet  21014  cnmpt2pc  21163  iihalf1  21166  iihalf2  21168  icoopnst  21174  iocopnst  21175  cphsqrtcl3  21369  cph2ass  21394  caublcls  21482  bcthlem3  21500  bcthlem4  21501  srabn  21535  rrxmet  21570  iblconst  21959  tdeglem3  22192  mdegmullem  22213  dvdsq1p  22296  coeid3  22372  aannenlem2  22459  pserdvlem2  22557  tanord1  22657  efgh  22661  cxpef  22774  recxpcl  22784  lawcos  22876  pythag  22877  isosctrlem1  22880  isosctrlem2  22881  ax5seglem1  23907  axcontlem2  23944  axcontlem8  23950  fiusgraedgfi  24083  nbgraf1olem3  24119  nb3graprlem2  24128  cusgra3v  24140  cusgrasizeindslem3  24151  cusgrasizeinds  24152  iswlkon  24210  istrlon  24219  2trllemE  24231  usgrnloop  24241  ispthon  24254  isspthon  24261  usgra2adedgwlkonALT  24292  usgrcyclnl2  24317  3v3e3cycl1  24320  constr3lem4  24323  constr3lem5  24324  constr3lem6  24325  constr3trllem2  24327  constr3trllem3  24328  4cycl4dv  24343  wwlkextproplem3  24419  clwwlkgt0  24447  clwwlknndef  24449  clwwlknfi  24454  clwlkisclwwlklem2a4  24460  clwlkisclwwlklem2a  24461  clwwlkel  24469  clwwlkext2edg  24478  clwwisshclwwlem1  24481  clwwnisshclwwn  24485  erclwwlktr  24491  erclwwlkntr  24503  clwlkfclwwlk  24520  clwlkfoclwwlk  24521  usg2wlkonot  24559  usg2wotspth  24560  2spontn0vne  24563  nbhashnn0  24590  nbhashuvtx  24592  usgrauvtxvdbi  24596  rusgra0edg  24631  frgra3v  24678  usg2spot2nb  24742  numclwlk3lem3  24750  extwwlkfablem2  24755  numclwwlkovf2ex  24763  numclwwlkovgelim  24766  numclwwlk4  24787  numclwwlk5lem  24788  numclwwlk5  24789  numclwwlk6  24790  numclwwlk7  24791  isgrpo  24874  grpoinvid1  24908  grpoinvid2  24909  grpoasscan1  24915  grpoasscan2  24916  grpoinvop  24919  grpodivinv  24922  grpoinvdiv  24923  grpodivf  24924  grpopncan  24929  grponpcan  24930  grpopnpcan2  24931  gxid  24951  resgrprn  24958  ablonncan  24972  zerdivemp1  25112  vcnegsubdi2  25144  vcsub4  25145  nvmval  25213  nvmval2  25214  nvmfval  25215  nvmul0or  25223  nvsubadd  25226  nvpncan2  25227  nvaddsub4  25232  nvnncan  25234  nvmeq0  25235  nvdif  25244  nvpi  25245  nvmtri  25250  nvabs  25252  imsmetlem  25272  ipval2lem3  25291  ipval2  25293  4ipval2  25294  ipval3  25295  ipval2lem6  25297  nmooge0  25358  blometi  25394  hvaddsub12  25631  hvsubdistr1  25642  hvsubdistr2  25643  hvaddcan2  25664  hvmulcan  25665  hvmulcan2  25666  hvsubcan  25667  hvsubcan2  25668  his7  25683  his2sub  25685  his2sub2  25686  norm3dif2  25744  shsubcl  25814  hhssnv  25856  shlej2  25955  fh2  26213  cm2j  26214  pjoi0  26311  hodcl  26342  hosubdi  26403  unopf1o  26511  unopadj  26514  adj2  26529  braadd  26540  bramul  26541  lnopaddmuli  26568  lnopsubmuli  26570  homco2  26572  lnfnaddmuli  26640  adjlnop  26681  leopmul  26729  leoptr  26732  pjimai  26771  atcv1  26975  atexch  26976  atcvatlem  26980  fcoinvbr  27134  divnumden2  27276  xdivmul  27289  resvsca  27483  relogbcl  27658  logblt  27662  hasheuni  27731  difelsiga  27773  cndprobin  28013  bayesth  28018  sgn3da  28120  ghomf1olem  28509  lediv2aALT  28518  subdivcomb1  28580  fununiq  28777  dfrdg2  28805  wfrlem4  28923  sltres  29001  nobndlem8  29036  ltflcei  29620  ftc1anclem4  29670  areacirc  29689  clsun  29723  neiin  29727  filbcmb  29834  ismtybnd  29906  grpoeqdivid  29946  ghomco  29948  rngonegrmul  29958  zerdivemp1x  29961  rngohomco  29980  rngoisoco  29988  riscer  29994  intidl  30029  isfldidl  30068  mzprename  30286  dvdsrabdioph  30347  pell14qrdivcl  30405  monotoddzz  30483  dvdsabsmod0  30532  jm2.19lem2  30536  jm2.19  30539  dvconstbi  30839  unima  31019  upbdrech  31082  cncfshift  31212  cncfperiod  31217  cncfuni  31225  icccncfext  31226  itgspltprt  31297  stoweidlem3  31303  stoweidlem10  31310  stoweidlem19  31319  stoweidlem31  31331  stoweidlem34  31334  stoweidlem44  31344  fourierdlem41  31448  fourierdlem42  31449  fourierdlem51  31458  fourierdlem68  31475  fourierdlem89  31496  fourierdlem91  31498  fourierdlem92  31499  fourierdlem94  31501  fourierdlem113  31520  sigaraf  31537  sigarmf  31538  subsubelfzo0  31807  xpprsng  31985  nn0sumltlt  32003  invginvrid  32025  ply1sclrmsm  32056  linccl  32088  lincvalpr  32092  lincresunit3lem1  32153  lincresunit3  32155  reccot  32233  rectan  32234  chordthmALT  32813  isosctrlem1ALT  32814  lshpnelb  33781  opnlen0  33985  opcon3b  33993  opcon2b  33994  oplecon3b  33997  opltcon3b  34001  opltcon2b  34003  oldmm1  34014  oldmm4  34017  oldmj1  34018  oldmj4  34021  cvrval2  34071  cvrcon3b  34074  leatb  34089  atcmp  34108  atcvreq0  34111  atlatle  34117  athgt  34252  3dim2  34264  islln2a  34313  lplnnleat  34338  lvolnleat  34379  4atlem10  34402  4atlem11  34405  4atlem12  34408  dalem21  34490  dalem22  34491  dalem23  34492  dalem29  34497  dalem30  34498  dalem31N  34499  dalem32  34500  dalem33  34501  dalem34  34502  dalem35  34503  dalem36  34504  dalem37  34505  dalem40  34508  dalem46  34514  dalem47  34515  dalem51  34519  dalem52  34520  dalem58  34526  dalem59  34527  pmaple  34557  paddclN  34638  pmapjoin  34648  pmapjat1  34649  elpcliN  34689  pclssN  34690  pclun2N  34695  2polcon4bN  34714  paddunN  34723  poldmj1N  34724  pmapj2N  34725  pmapocjN  34726  psubclinN  34744  paddatclN  34745  poml4N  34749  lautco  34893  ldilco  34912  ltrneq2  34944  trljat1  34962  cdlemc1  34987  cdleme10  35050  ltrnco  35515  trlcocnv  35516  trljco  35536  trljco2  35537  cdlemi1  35614  tendocnv  35818  diaord  35844  dibord  35956  dihord3  36054  dihord4  36055  dihmeetlem2N  36096  dihmeetlem4preN  36103  dochdmj1  36187  hdmap10lem  36639
  Copyright terms: Public domain W3C validator