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

Theorem 3adant2 1000
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 979 . 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 958
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 960
This theorem is referenced by:  3ad2ant1  1002  eupickb  2340  eupickbOLD  2341  vtoclegft  3033  eqeu  3119  funopg  5438  fnco  5507  dff1o2  5634  fnimapr  5743  fvmptt  5777  fnreseql  5801  f1elima  5963  f1ocnvfvb  5973  oprssov  6221  ordunel  6427  poxp  6673  smoiso  6809  oaord  6974  oaword  6976  omcan  6996  omwordri  6999  odi  7006  omeulem1  7009  oeord  7015  oecan  7016  oewordri  7019  oeordsuc  7021  nnaord  7046  nnaordr  7047  nndi  7050  nnaword  7054  nnmwordri  7063  erov  7185  ecopovtrn  7191  xpdom3  7397  mapxpen  7465  findcard  7539  indexfi  7607  suppr  7706  r111  7970  tcrank  8079  acndom  8209  infdif2  8367  infxpdom  8368  cfeq0  8413  cfsuc  8414  cfflb  8416  cflim2  8420  cfsmolem  8427  axcc3  8595  domtriomlem  8599  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  axcclem  8614  pwcfsdom  8735  tsktrss  8916  tsksuc  8917  tskuni  8938  adderpqlem  9111  mulerpqlem  9112  mulcanenq  9117  distrnq  9118  ltsonq  9126  ltanq  9128  ltmnq  9129  distrlem1pr  9182  distrlem5pr  9184  ltsopr  9189  ltsosr  9249  ltasr  9255  adddir  9365  axlttrn  9435  letr  9456  ltneOLD  9460  nnncan1  9633  npncan3  9635  pnpcan2  9637  subdi  9766  subdir  9767  mulcan1g  9977  mulcan2g  9978  divmul  9985  div23  10001  div13  10003  divsubdir  10015  divcan7  10028  ltmul2  10168  lemul1  10169  lemul2  10170  lemul2a  10172  lediv1  10182  ltmuldiv2  10191  lemuldiv  10199  lemuldiv2  10200  ltdiv2  10205  lediv2  10210  infmrlb  10299  nndivtr  10351  bndndx  10566  nn0n0n1ge2  10631  fnn0ind  10729  lbzbi  10931  xrletr  11120  qsqueeze  11159  xleadd2a  11205  xleadd1  11206  xltadd2  11208  xltmul2  11244  supxrbnd  11279  iooneg  11392  iccneg  11393  icoshft  11394  icoshftf1o  11395  fzen  11454  uzsubsubfz  11458  fz0fzdiffz0  11476  elfzmlbm  11477  elfzmlbp  11478  fzrevral2  11529  fzshftral  11531  elfzo  11539  fzoaddel2  11582  fzosubel2  11584  ssfzo12bi  11606  fzonfzoufzol  11612  flltdivnn0lt  11661  modmulnn  11709  modcyc  11727  modaddabs  11730  modaddmod  11731  modadd2mod  11733  modsubmod  11741  modsubmodmod  11742  modaddmodup  11746  modmulmod  11748  moddi  11750  modsubdir  11751  uzindi  11787  axdc4uzlem  11788  expneg2  11858  expdiv  11898  expubnd  11908  bernneq2  11975  hashinfxadd  12132  brfi1indlem  12202  ccatsymb  12265  ccatfv0  12266  ccats1val2  12291  swrdnd  12310  swrdvalodm2  12317  2swrd1eqwrdeq  12332  swrdswrd  12338  wrd2ind  12356  swrdccatin1  12358  swrdccatin12lem2b  12361  swrdccatin2  12362  swrdccatin12lem2  12364  swrdccatin12lem3  12365  swrdccat  12368  swrdccat3a  12369  swrdccat3blem  12370  repswswrd  12406  repswccat  12407  cshwidxmod  12424  2cshw  12431  3cshw  12436  ccatco  12447  cshco  12448  swrdco  12449  lswco  12450  swrds2  12529  2swrd2eqwrdeq  12537  shftuz  12542  shftval2  12548  abs3dif  12803  sin02gt0  13459  dvdsval2  13521  dvdscmul  13542  dvdsmulc  13543  dvdscmulr  13544  dvdsmulcr  13545  divalglem8  13587  ndvdssub  13594  rpmulgcd  13722  isprm3  13755  coprmdvds  13771  modprm0  13856  coprimeprodsq  13859  pythagtriplem12  13876  pythagtriplem14  13878  pcprendvds  13890  pcmul  13901  pcdiv  13902  pcqcl  13906  pcqdiv  13907  pcdvdsb  13918  pcgcd  13927  vdwnnlem1  14039  hashbcss  14048  cshwshashlem1  14105  fvsetsid  14182  mrcss  14537  mrcsscl  14541  mrcun  14543  cofulid  14783  catcisolem  14957  latleeqj1  15216  lubun  15276  clatleglb  15279  pslem  15359  dirtr  15389  pwspjmhm  15478  gsumccat  15499  grpinvid1  15566  grpinvid2  15567  grpinvadd  15584  grpsubf  15585  grpsubrcan  15587  grpinvsub  15588  grpsubeq0  15592  grppncan  15596  grpnpcan  15597  mulgnn0p1  15618  subgsubcl  15672  subgsub  15673  eqglact  15712  divssub  15721  ghmsub  15735  psgnunilem4  15983  oddvds2  16047  odsubdvds  16050  gexnnod  16067  slwn0  16094  gsumsn  16425  gsumdixpOLD  16635  gsumdixp  16636  dvrcl  16712  unitdvcl  16713  dvrcan1  16717  dvrcan3  16718  dvreq1  16719  subrgdv  16806  abvsubtri  16844  idsrngd  16871  lmodvsubval2  16924  lsmcl  17086  lsmsp2  17090  lspsntrim  17101  lidldvgen  17259  evlslem4OLD  17518  evlslem4  17519  chrcong  17802  zndvds  17824  zntoslem  17831  ocvsscon  17942  obselocv  17995  frlmphl  18048  mamudm  18130  mamufacex  18131  submabas  18231  mdetralt2  18257  mdetero  18258  mdetunilem2  18261  mdetunilem6  18265  m2detleiblem7  18275  maducoeval2  18288  gsummatr01lem3  18305  gsummatr01  18307  smadiadetglem2  18320  cramerlem1  18335  istps3OLD  18369  ntrin  18507  elnei  18557  neindisj2  18569  ordtopn3  18642  ordtcld3  18645  leordtval2  18658  lecldbas  18665  cnrest2  18732  cmpsublem  18844  ptrescn  19054  xkococn  19075  kqfeq  19139  snfbas  19281  neifil  19295  fclsrest  19439  utopsnnei  19666  neipcfilu  19713  psmetsym  19728  psmetge0  19730  xmetge0  19761  xmetsym  19764  metusttoOLD  19974  metustto  19975  metustblOLD  19997  metustbl  19998  restmetu  20004  nm2dif  20058  nmtri  20059  cnmet  20193  cnmpt2pc  20342  iihalf1  20345  iihalf2  20347  icoopnst  20353  iocopnst  20354  cphsqrcl3  20548  cph2ass  20573  caublcls  20661  bcthlem3  20679  bcthlem4  20680  srabn  20714  rrxmet  20749  iblconst  21137  mpfsubrg  21392  tdeglem3  21413  mdegmullem  21434  dvdsq1p  21517  coeid3  21593  aannenlem2  21680  pserdvlem2  21778  tanord1  21878  efgh  21882  cxpef  21995  recxpcl  22005  lawcos  22097  pythag  22098  isosctrlem1  22101  isosctrlem2  22102  ax5seglem1  22997  axcontlem2  23034  axcontlem8  23040  fiusgraedgfi  23143  nbgraf1olem3  23175  nb3graprlem2  23183  cusgra3v  23195  cusgrasizeindslem3  23206  cusgrasizeinds  23207  iswlkon  23253  istrlon  23263  2trllemE  23275  usgrnloop  23285  ispthon  23298  isspthon  23305  usgrcyclnl2  23350  3v3e3cycl1  23353  constr3lem4  23356  constr3lem5  23357  constr3lem6  23358  constr3trllem2  23360  constr3trllem3  23361  4cycl4dv  23376  isgrpo  23506  grpoinvid1  23540  grpoinvid2  23541  grpoasscan1  23547  grpoasscan2  23548  grpoinvop  23551  grpodivinv  23554  grpoinvdiv  23555  grpodivf  23556  grpopncan  23561  grponpcan  23562  grpopnpcan2  23563  gxid  23583  resgrprn  23590  ablonncan  23604  zerdivemp1  23744  vcnegsubdi2  23776  vcsub4  23777  nvmval  23845  nvmval2  23846  nvmfval  23847  nvmul0or  23855  nvsubadd  23858  nvpncan2  23859  nvaddsub4  23864  nvnncan  23866  nvmeq0  23867  nvdif  23876  nvpi  23877  nvmtri  23882  nvabs  23884  imsmetlem  23904  ipval2lem3  23923  ipval2  23925  4ipval2  23926  ipval3  23927  ipval2lem6  23929  nmooge0  23990  blometi  24026  hvaddsub12  24263  hvsubdistr1  24274  hvsubdistr2  24275  hvaddcan2  24296  hvmulcan  24297  hvmulcan2  24298  hvsubcan  24299  hvsubcan2  24300  his7  24315  his2sub  24317  his2sub2  24318  norm3dif2  24376  shsubcl  24446  hhssnv  24488  shlej2  24587  fh2  24845  cm2j  24846  pjoi0  24943  hodcl  24974  hosubdi  25035  unopf1o  25143  unopadj  25146  adj2  25161  braadd  25172  bramul  25173  lnopaddmuli  25200  lnopsubmuli  25202  homco2  25204  lnfnaddmuli  25272  adjlnop  25313  leopmul  25361  leoptr  25364  pjimai  25403  atcv1  25607  atexch  25608  atcvatlem  25612  divnumden2  25910  xdivmul  25923  gsumsnf  26096  resvsca  26152  relogbcl  26315  logblt  26319  hasheuni  26388  difelsiga  26430  cndprobin  26665  bayesth  26670  sgn3da  26772  ghomf1olem  27160  lediv2aALT  27169  subdivcomb1  27231  fununiq  27428  dfrdg2  27456  wfrlem4  27574  sltres  27652  nobndlem8  27687  ltflcei  28263  ftc1anclem4  28314  areacirc  28333  clsun  28367  neiin  28371  filbcmb  28478  ismtybnd  28550  grpoeqdivid  28590  ghomco  28592  rngonegrmul  28602  zerdivemp1x  28605  rngohomco  28624  rngoisoco  28632  riscer  28638  intidl  28673  isfldidl  28712  mzprename  28931  dvdsrabdioph  28993  pell14qrdivcl  29051  monotoddzz  29129  dvdsabsmod0  29180  jm2.19lem2  29184  jm2.19  29187  dvconstbi  29453  stoweidlem3  29644  stoweidlem10  29651  stoweidlem19  29660  stoweidlem31  29672  stoweidlem34  29675  stoweidlem44  29685  sigaraf  29735  sigarmf  29736  f13dfv  29993  subsubelfzo0  30056  elfzom1p1elfzo  30061  elfzom1elp1fzo  30064  modfsummods  30090  mulmoddvds  30092  usg2wlkonot  30248  usg2wotspth  30249  2spontn0vne  30252  clwwlkgt0  30280  clwwlknndef  30282  clwlkisclwwlklem2a4  30292  clwlkisclwwlklem2a  30293  clwwlkel  30301  clwwlkext2edg  30310  clwwisshclwwlem1  30315  clwwnisshclwwn  30319  clwwlknfi  30323  erclwwlktr0  30325  erclwwlktr  30331  scshwfzeqfzo  30338  erclwwlkntr  30347  clwlkfclwwlk  30363  clwlkfoclwwlk  30364  nbhashnn0  30378  nbhashuvtx  30380  usgrauvtxvdbi  30382  wwlkextproplem3  30408  rusgra0edg  30419  frgra3v  30440  usg2spot2nb  30504  numclwlk3lem3  30512  extwwlkfablem2  30517  numclwwlkovf2ex  30525  numclwwlkovgelim  30528  numclwwlk4  30549  numclwwlk5lem  30550  numclwwlk5  30551  numclwwlk6  30552  numclwwlk7  30553  xpprsng  30564  invginvrid  30603  linccl  30657  lincvalpr  30661  lincresunit3lem1  30722  lincresunit3  30724  reccot  30802  rectan  30803  chordthmALT  31371  isosctrlem1ALT  31372  lshpnelb  32202  opnlen0  32406  opcon3b  32414  opcon2b  32415  oplecon3b  32418  opltcon3b  32422  opltcon2b  32424  oldmm1  32435  oldmm4  32438  oldmj1  32439  oldmj4  32442  cvrval2  32492  cvrcon3b  32495  leatb  32510  atcmp  32529  atcvreq0  32532  atlatle  32538  athgt  32673  3dim2  32685  islln2a  32734  lplnnleat  32759  lvolnleat  32800  4atlem10  32823  4atlem11  32826  4atlem12  32829  dalem21  32911  dalem22  32912  dalem23  32913  dalem29  32918  dalem30  32919  dalem31N  32920  dalem32  32921  dalem33  32922  dalem34  32923  dalem35  32924  dalem36  32925  dalem37  32926  dalem40  32929  dalem46  32935  dalem47  32936  dalem51  32940  dalem52  32941  dalem58  32947  dalem59  32948  pmaple  32978  paddclN  33059  pmapjoin  33069  pmapjat1  33070  elpcliN  33110  pclssN  33111  pclun2N  33116  2polcon4bN  33135  paddunN  33144  poldmj1N  33145  pmapj2N  33146  pmapocjN  33147  psubclinN  33165  paddatclN  33166  poml4N  33170  lautco  33314  ldilco  33333  ltrneq2  33365  trljat1  33383  cdlemc1  33408  cdleme10  33471  ltrnco  33936  trlcocnv  33937  trljco  33957  trljco2  33958  cdlemi1  34035  tendocnv  34239  diaord  34265  dibord  34377  dihord3  34475  dihord4  34476  dihmeetlem2N  34517  dihmeetlem4preN  34524  dochdmj1  34608  hdmap10lem  35060
  Copyright terms: Public domain W3C validator