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

Theorem 3adant2 1016
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 995 . 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 974
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 976
This theorem is referenced by:  3ad2ant1  1018  eupickb  2346  vtoclegft  3167  eqeu  3256  funopg  5610  fnco  5679  dff1o2  5811  fnimapr  5922  fvmptt  5956  fnreseql  5982  f1elima  6156  f13dfv  6165  f1ocnvfvb  6170  oprssov  6429  ordunel  6647  poxp  6897  smoiso  7035  oaord  7198  oaword  7200  omcan  7220  omwordri  7223  odi  7230  omeulem1  7233  oeord  7239  oecan  7240  oewordri  7243  oeordsuc  7245  nnaord  7270  nnaordr  7271  nndi  7274  nnaword  7278  nnmwordri  7287  erov  7410  ecopovtrn  7416  xpdom3  7617  mapxpen  7685  findcard  7761  indexfi  7830  suppr  7932  r111  8196  tcrank  8305  acndom  8435  infdif2  8593  infxpdom  8594  cfeq0  8639  cfsuc  8640  cfflb  8642  cflim2  8646  cfsmolem  8653  axcc3  8821  domtriomlem  8825  axdc3lem2  8834  axdc3lem4  8836  axdc4lem  8838  axcclem  8840  pwcfsdom  8961  tsktrss  9142  tsksuc  9143  tskuni  9164  adderpqlem  9335  mulerpqlem  9336  mulcanenq  9341  distrnq  9342  ltsonq  9350  ltanq  9352  ltmnq  9353  distrlem1pr  9406  distrlem5pr  9408  ltsopr  9413  ltsosr  9474  ltasr  9480  adddir  9590  axlttrn  9660  letr  9681  ltneOLD  9685  nnncan1  9860  npncan3  9862  pnpcan2  9864  subdi  9996  subdir  9997  mulcan1g  10208  mulcan2g  10209  divmul  10216  div23  10232  div13  10234  divsubdir  10246  divcan7  10259  ltmul2  10399  lemul1  10400  lemul2  10401  lemul2a  10403  lediv1  10413  ltmuldiv2  10422  lemuldiv  10430  lemuldiv2  10431  ltdiv2  10436  lediv2  10441  infmrlb  10530  nndivtr  10583  bndndx  10800  nn0n0n1ge2  10865  fnn0ind  10968  xrletr  11370  qsqueeze  11409  xleadd2a  11455  xleadd1  11456  xltadd2  11458  xltmul2  11494  supxrbnd  11529  iooneg  11649  iccneg  11650  icoshft  11651  icoshftf1o  11652  fzen  11712  uzsubsubfz  11716  fzrevral2  11772  fzshftral  11774  fz0fzdiffz0  11791  elfzmlbmOLD  11793  elfzmlbp  11794  elfzo  11810  fzoaddel2  11853  fzosubel2  11855  elfzom1p1elfzo  11874  ssfzo12bi  11886  fzonfzoufzol  11892  flltdivnn0lt  11944  modmulnn  11992  modcyc  12010  modaddabs  12013  modaddmod  12014  modadd2mod  12016  modsubmod  12024  modsubmodmod  12025  modaddmodup  12029  modmulmod  12031  moddi  12033  modsubdir  12034  uzindi  12070  axdc4uzlem  12071  expneg2  12154  expdiv  12195  expubnd  12205  bernneq2  12272  hashinfxadd  12432  brfi1indlem  12510  ccatsymb  12579  ccatfv0  12580  ccats1val2  12610  swrdnd  12636  swrdvalodm2  12643  2swrd1eqwrdeq  12658  swrdswrd  12664  wrd2ind  12682  swrdccatin1  12687  swrdccatin12lem2b  12690  swrdccatin2  12691  swrdccatin12lem2  12693  swrdccatin12lem3  12694  swrdccat  12697  swrdccat3a  12698  swrdccat3blem  12699  repswswrd  12735  repswccat  12736  cshwidxmod  12753  2cshw  12760  3cshw  12765  scshwfzeqfzo  12773  cshwcsh2id  12775  ccatco  12780  cshco  12781  swrdco  12782  lswco  12783  swrds2  12862  2swrd2eqwrdeq  12870  shftuz  12881  shftval2  12887  abs3dif  13143  modfsummods  13586  sin02gt0  13804  dvdsval2  13866  dvdscmul  13887  dvdsmulc  13888  dvdscmulr  13889  dvdsmulcr  13890  mulmoddvds  13921  divalglem8  13935  ndvdssub  13942  rpmulgcd  14070  isprm3  14103  coprmdvds  14120  modprm0  14207  coprimeprodsq  14210  pythagtriplem12  14227  pythagtriplem14  14229  pcprendvds  14241  pcmul  14252  pcdiv  14253  pcqcl  14257  pcqdiv  14258  pcdvdsb  14269  pcgcd  14278  vdwnnlem1  14390  hashbcss  14399  cshwshashlem1  14457  fvsetsid  14534  mrcss  14890  mrcsscl  14894  mrcun  14896  cofulid  15133  catcisolem  15307  latleeqj1  15567  lubun  15627  clatleglb  15630  pslem  15710  dirtr  15740  mgmb1mgm1  15757  pwspjmhm  15873  gsumccat  15883  grpinvid1  15972  grpinvid2  15973  grpinvadd  15990  grpsubf  15991  grpsubrcan  15993  grpinvsub  15994  grpsubeq0  15998  grpsubadd0sub  15999  grppncan  16003  grpnpcan  16004  mulgnn0p1  16027  subgsubcl  16086  subgsub  16087  eqglact  16126  qussub  16135  ghmsub  16149  psgnunilem4  16396  oddvds2  16462  odsubdvds  16465  gexnnod  16482  slwn0  16509  gsumdixpOLD  17131  gsumdixp  17132  dvrcl  17209  unitdvcl  17210  dvrcan1  17214  dvrcan3  17215  dvreq1  17216  subrgdv  17320  abvsubtri  17358  idsrngd  17385  lmodvsubval2  17439  lsmcl  17603  lsmsp2  17607  lspsntrim  17618  lidldvgen  17777  evlslem4OLD  18047  evlslem4  18048  mpfsubrg  18075  ply1tmcl  18187  eqcoe1ply1eq  18213  gsummoncoe1  18220  lply1binomsc  18223  chrcong  18439  zndvds  18461  zntoslem  18468  ocvsscon  18579  obselocv  18632  frlmphl  18685  mamudm  18763  mamufacex  18764  scmatf1  18906  scmatf1o  18907  scmatrngiso  18911  submabas  18953  mdetdiaglem  18973  mdetralt2  18984  mdetero  18985  mdetunilem2  18988  mdetunilem6  18992  m2detleiblem7  19002  maducoeval2  19015  gsummatr01lem3  19032  gsummatr01  19034  smadiadetglem2  19047  cramerlem1  19062  mply1topmatcl  19179  mp2pm2mplem4  19183  istps3OLD  19296  ntrin  19435  elnei  19485  neindisj2  19497  ordtopn3  19570  ordtcld3  19573  leordtval2  19586  lecldbas  19593  cnrest2  19660  cmpsublem  19772  ptrescn  20013  xkococn  20034  kqfeq  20098  snfbas  20240  neifil  20254  fclsrest  20398  utopsnnei  20625  neipcfilu  20672  psmetsym  20687  psmetge0  20689  xmetge0  20720  xmetsym  20723  metusttoOLD  20933  metustto  20934  metustblOLD  20956  metustbl  20957  restmetu  20963  nm2dif  21017  nmtri  21018  cnmet  21152  cnmpt2pc  21301  iihalf1  21304  iihalf2  21306  iocopnst  21313  cphsqrtcl3  21507  cph2ass  21532  caublcls  21620  bcthlem3  21638  bcthlem4  21639  srabn  21673  rrxmet  21708  iblconst  22097  tdeglem3  22330  mdegmullem  22351  dvdsq1p  22434  coeid3  22510  aannenlem2  22597  pserdvlem2  22695  tanord1  22796  cxpef  22918  recxpcl  22928  lawcos  23020  pythag  23021  isosctrlem1  23024  isosctrlem2  23025  ax5seglem1  24103  axcontlem2  24140  axcontlem8  24146  fiusgraedgfi  24279  nbgraf1olem3  24315  nb3graprlem2  24324  cusgra3v  24336  cusgrasizeindslem3  24347  cusgrasizeinds  24348  iswlkon  24406  istrlon  24415  2trllemE  24427  usgrnloop  24437  ispthon  24450  isspthon  24457  usgra2adedgwlkonALT  24488  usgrcyclnl2  24513  3v3e3cycl1  24516  constr3lem4  24519  constr3lem5  24520  constr3lem6  24521  constr3trllem2  24523  constr3trllem3  24524  4cycl4dv  24539  wwlkextproplem3  24615  clwwlkgt0  24643  clwwlknndef  24645  clwwlknfi  24650  clwlkisclwwlklem2a4  24656  clwlkisclwwlklem2a  24657  clwwlkel  24665  clwwlkext2edg  24674  clwwisshclwwlem1  24677  clwwnisshclwwn  24681  erclwwlktr  24687  erclwwlkntr  24699  clwlkfclwwlk  24716  clwlkfoclwwlk  24717  usg2wotspth  24756  2spontn0vne  24759  nbhashnn0  24786  nbhashuvtx  24788  usgrauvtxvdbi  24792  rusgra0edg  24827  frgra3v  24874  usg2spot2nb  24937  numclwlk3lem3  24945  extwwlkfablem2  24950  numclwwlkovf2ex  24958  numclwwlkovgelim  24961  numclwwlk4  24982  numclwwlk5lem  24983  numclwwlk5  24984  numclwwlk6  24985  numclwwlk7  24986  isgrpo  25070  grpoinvid1  25104  grpoinvid2  25105  grpoasscan1  25111  grpoasscan2  25112  grpoinvop  25115  grpodivinv  25118  grpoinvdiv  25119  grpodivf  25120  grpopncan  25125  grponpcan  25126  grpopnpcan2  25127  gxid  25147  resgrprn  25154  ablonncan  25168  zerdivemp1  25308  vcnegsubdi2  25340  vcsub4  25341  nvmval  25409  nvmval2  25410  nvmfval  25411  nvmul0or  25419  nvsubadd  25422  nvpncan2  25423  nvaddsub4  25428  nvnncan  25430  nvmeq0  25431  nvdif  25440  nvpi  25441  nvmtri  25446  nvabs  25448  imsmetlem  25468  ipval2lem3  25487  ipval2  25489  4ipval2  25490  ipval3  25491  ipval2lem6  25493  nmooge0  25554  blometi  25590  hvaddsub12  25827  hvsubdistr1  25838  hvsubdistr2  25839  hvaddcan2  25860  hvmulcan  25861  hvmulcan2  25862  hvsubcan  25863  hvsubcan2  25864  his7  25879  his2sub  25881  his2sub2  25882  norm3dif2  25940  shsubcl  26010  hhssnv  26052  shlej2  26151  fh2  26409  cm2j  26410  pjoi0  26507  hodcl  26538  hosubdi  26599  unopf1o  26707  unopadj  26710  adj2  26725  braadd  26736  bramul  26737  lnopaddmuli  26764  lnopsubmuli  26766  homco2  26768  lnfnaddmuli  26836  adjlnop  26877  leopmul  26925  leoptr  26928  pjimai  26967  atcv1  27171  atexch  27172  atcvatlem  27176  fcoinvbr  27333  divnumden2  27481  xdivmul  27494  resvsca  27693  relogbcl  27891  logblt  27895  hasheuni  27964  difelsiga  28006  cndprobin  28246  bayesth  28251  sgn3da  28353  ghomf1olem  28907  lediv2aALT  28916  subdivcomb1  28978  fununiq  29175  dfrdg2  29203  wfrlem4  29321  sltres  29399  nobndlem8  29434  ftc1anclem4  30068  areacirc  30087  clsun  30121  neiin  30125  filbcmb  30206  ismtybnd  30278  grpoeqdivid  30318  ghomco  30320  rngonegrmul  30330  zerdivemp1x  30333  rngohomco  30352  rngoisoco  30360  riscer  30366  intidl  30401  isfldidl  30440  mzprename  30657  dvdsrabdioph  30718  pell14qrdivcl  30776  monotoddzz  30854  dvdsabsmod0  30903  jm2.19lem2  30907  jm2.19  30910  dvconstbi  31215  unima  31391  upbdrech  31454  cncfshift  31583  cncfperiod  31588  cncfuni  31596  icccncfext  31597  itgspltprt  31668  stoweidlem3  31674  stoweidlem10  31681  stoweidlem19  31690  stoweidlem31  31702  stoweidlem34  31705  stoweidlem44  31715  fourierdlem41  31819  fourierdlem42  31820  fourierdlem51  31829  fourierdlem68  31846  fourierdlem89  31867  fourierdlem91  31869  fourierdlem92  31870  fourierdlem94  31872  sigaraf  31908  sigarmf  31909  subsubelfzo0  32176  xpprsng  32654  nn0sumltlt  32672  invginvrid  32693  ply1sclrmsm  32718  linccl  32750  lincvalpr  32754  lincresunit3lem1  32815  lincresunit3  32817  reccot  32887  rectan  32888  chordthmALT  33466  isosctrlem1ALT  33467  lshpnelb  34449  opnlen0  34653  opcon3b  34661  opcon2b  34662  oplecon3b  34665  opltcon3b  34669  opltcon2b  34671  oldmm1  34682  oldmm4  34685  oldmj1  34686  oldmj4  34689  cvrval2  34739  cvrcon3b  34742  leatb  34757  atcmp  34776  atcvreq0  34779  atlatle  34785  athgt  34920  3dim2  34932  islln2a  34981  lplnnleat  35006  lvolnleat  35047  4atlem10  35070  4atlem11  35073  4atlem12  35076  dalem21  35158  dalem22  35159  dalem23  35160  dalem29  35165  dalem30  35166  dalem31N  35167  dalem32  35168  dalem33  35169  dalem34  35170  dalem35  35171  dalem36  35172  dalem37  35173  dalem40  35176  dalem46  35182  dalem47  35183  dalem51  35187  dalem52  35188  dalem58  35194  dalem59  35195  pmaple  35225  paddclN  35306  pmapjoin  35316  pmapjat1  35317  elpcliN  35357  pclssN  35358  pclun2N  35363  2polcon4bN  35382  paddunN  35391  poldmj1N  35392  pmapj2N  35393  pmapocjN  35394  psubclinN  35412  paddatclN  35413  poml4N  35417  lautco  35561  ldilco  35580  ltrneq2  35612  trljat1  35631  cdlemc1  35656  cdleme10  35719  ltrnco  36185  trlcocnv  36186  trljco  36206  trljco2  36207  cdlemi1  36284  tendocnv  36488  diaord  36514  dibord  36626  dihord3  36724  dihord4  36725  dihmeetlem2N  36766  dihmeetlem4preN  36773  dochdmj1  36857  hdmap10lem  37309
  Copyright terms: Public domain W3C validator