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

Theorem 3adant2 976
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 955 . 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 set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ad2ant1  978  eupickb  2319  vtoclegft  2983  eqeu  3065  ordunel  4766  funopg  5444  fnco  5512  dff1o2  5638  fnimapr  5746  fvmptt  5779  fnreseql  5799  f1elima  5968  f1ocnvfvb  5976  oprssov  6174  poxp  6417  smoiso  6583  oaord  6749  oaword  6751  omcan  6771  omwordri  6774  odi  6781  omeulem1  6784  oeord  6790  oecan  6791  oewordri  6794  oeordsuc  6796  nnaord  6821  nnaordr  6822  nndi  6825  nnaword  6829  nnmwordri  6838  erov  6960  ecopovtrn  6966  xpdom3  7165  mapxpen  7232  findcard  7306  indexfi  7372  suppr  7429  r111  7657  tcrank  7764  acndom  7888  infdif2  8046  infxpdom  8047  cfeq0  8092  cfsuc  8093  cfflb  8095  cflim2  8099  cfsmolem  8106  axcc3  8274  domtriomlem  8278  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  pwcfsdom  8414  tsktrss  8592  tsksuc  8593  tskuni  8614  adderpqlem  8787  mulerpqlem  8788  mulcanenq  8793  distrnq  8794  ltsonq  8802  ltanq  8804  ltmnq  8805  distrlem1pr  8858  distrlem5pr  8860  ltsopr  8865  ltsosr  8925  ltasr  8931  adddir  9039  axlttrn  9104  letr  9123  ltneOLD  9127  nnncan1  9293  npncan3  9295  pnpcan2  9297  subdi  9423  subdir  9424  divmul  9637  div23  9653  div13  9655  divsubdir  9666  divcan7  9679  ltmul2  9817  lemul1  9818  lemul2  9819  lemul2a  9821  lediv1  9831  ltmuldiv2  9837  lemuldiv  9845  lemuldiv2  9846  ltdiv2  9851  lediv2  9856  infmrlb  9945  nndivtr  9997  bndndx  10176  nn0n0n1ge2  10236  fnn0ind  10325  lbzbi  10520  xrletr  10704  qsqueeze  10743  xleadd2a  10789  xleadd1  10790  xltadd2  10792  xltmul2  10828  supxrbnd  10863  iooneg  10973  iccneg  10974  icoshft  10975  icoshftf1o  10976  fzen  11028  fzrevral2  11087  fzshftral  11089  elfzo  11097  fzoaddel2  11131  fzosubel2  11133  modmulnn  11220  modcyc  11231  moddi  11239  modsubdir  11240  uzindi  11275  axdc4uzlem  11276  expneg2  11345  expdiv  11385  expubnd  11395  bernneq2  11461  hashinfxadd  11614  brfi1indlem  11669  ccatco  11759  swrds2  11835  shftuz  11839  shftval2  11845  abs3dif  12090  sin02gt0  12748  dvdsval2  12810  dvdscmul  12831  dvdsmulc  12832  dvdscmulr  12833  dvdsmulcr  12834  divalglem8  12875  ndvdssub  12882  rpmulgcd  13010  isprm3  13043  coprmdvds  13057  coprimeprodsq  13138  pythagtriplem12  13155  pythagtriplem14  13157  pcprendvds  13169  pcmul  13180  pcdiv  13181  pcqcl  13185  pcqdiv  13186  pcdvdsb  13197  pcgcd  13206  vdwnnlem1  13318  hashbcss  13327  mrcss  13796  mrcsscl  13800  mrcun  13802  cofulid  14042  catcisolem  14216  ple1  14428  latleeqj1  14447  clatl  14498  lubun  14505  clatleglb  14508  pslem  14593  dirtr  14636  pwspjmhm  14722  gsumccat  14742  grpinvid1  14808  grpinvid2  14809  grpinvadd  14822  grpsubf  14823  grpsubrcan  14825  grpinvsub  14826  grpsubeq0  14830  grppncan  14834  grpnpcan  14835  mulgnn0p1  14856  subgsubcl  14910  subgsub  14911  eqglact  14946  divssub  14955  ghmsub  14969  odval2  15144  oddvds2  15157  odsubdvds  15160  gexnnod  15177  slwn0  15204  gsumsn  15498  gsumdixp  15670  dvrcl  15746  unitdvcl  15747  dvrcan1  15751  dvrcan3  15752  dvreq1  15753  subrgdv  15840  abvsubtri  15878  lmodvsubval2  15954  lsmcl  16110  lsmsp2  16114  lspsntrim  16125  lidldvgen  16281  evlslem4  16519  chrcong  16765  zndvds  16785  zntoslem  16792  ocvsscon  16857  obselocv  16910  istps3OLD  16942  ntrin  17080  elnei  17130  neindisj2  17142  ordtopn3  17214  ordtcld3  17217  leordtval2  17230  lecldbas  17237  cnrest2  17304  cmpsublem  17416  ptrescn  17624  xkococn  17645  kqfeq  17709  snfbas  17851  neifil  17865  fclsrest  18009  utopsnnei  18232  neipcfilu  18279  psmetsym  18294  psmetge0  18296  xmetge0  18327  xmetsym  18330  metusttoOLD  18540  metustto  18541  metustblOLD  18563  metustbl  18564  restmetu  18570  nm2dif  18624  nmtri  18625  cnmet  18759  cnmpt2pc  18906  iihalf1  18909  iihalf2  18911  icoopnst  18917  iocopnst  18918  cphsqrcl3  19103  cph2ass  19128  caublcls  19214  bcthlem3  19232  bcthlem4  19233  srabn  19267  iblconst  19662  mpfsubrg  19914  tdeglem3  19935  mdegmullem  19954  dvdsq1p  20036  coeid3  20112  aannenlem2  20199  pserdvlem2  20297  tanord1  20392  efgh  20396  cxpef  20509  recxpcl  20519  lawcos  20611  pythag  20612  isosctrlem1  20615  isosctrlem2  20616  fiusgraedgfi  21374  nbgraf1olem3  21406  nb3graprlem2  21414  cusgra3v  21426  cusgrasizeindslem3  21437  cusgrasizeinds  21438  iswlkon  21484  istrlon  21494  2trllemE  21506  usgrnloop  21516  ispthon  21529  isspthon  21536  usgrcyclnl2  21581  3v3e3cycl1  21584  constr3lem4  21587  constr3lem5  21588  constr3lem6  21589  constr3trllem2  21591  constr3trllem3  21592  4cycl4dv  21607  isgrpo  21737  grpoinvid1  21771  grpoinvid2  21772  grpoasscan1  21778  grpoasscan2  21779  grpoinvop  21782  grpodivinv  21785  grpoinvdiv  21786  grpodivf  21787  grpopncan  21792  grponpcan  21793  grpopnpcan2  21794  gxid  21814  resgrprn  21821  ablonncan  21835  zerdivemp1  21975  vcnegsubdi2  22007  vcsub4  22008  nvmval  22076  nvmval2  22077  nvmfval  22078  nvmul0or  22086  nvsubadd  22089  nvpncan2  22090  nvaddsub4  22095  nvnncan  22097  nvmeq0  22098  nvdif  22107  nvpi  22108  nvmtri  22113  nvabs  22115  imsmetlem  22135  ipval2lem3  22154  ipval2  22156  4ipval2  22157  ipval3  22158  ipval2lem6  22160  nmooge0  22221  blometi  22257  hvaddsub12  22493  hvsubdistr1  22504  hvsubdistr2  22505  hvaddcan2  22526  hvmulcan  22527  hvmulcan2  22528  hvsubcan  22529  hvsubcan2  22530  his7  22545  his2sub  22547  his2sub2  22548  norm3dif2  22606  shsubcl  22676  hhssnv  22717  shlej2  22816  fh2  23074  cm2j  23075  pjoi0  23172  hodcl  23203  hosubdi  23264  unopf1o  23372  unopadj  23375  adj2  23390  braadd  23401  bramul  23402  lnopaddmuli  23429  lnopsubmuli  23431  homco2  23433  lnfnaddmuli  23501  adjlnop  23542  leopmul  23590  leoptr  23593  pjimai  23632  atcv1  23836  atexch  23837  atcvatlem  23841  divnumden2  24114  xdivmul  24124  relogbcl  24355  logblt  24359  hasheuni  24428  difelsiga  24469  cndprobin  24645  bayesth  24650  ghomf1olem  25058  modaddabs  25068  lediv2aALT  25070  mulcan1g  25142  mulcan2g  25143  subdivcomb1  25148  fununiq  25340  dfrdg2  25366  wfrlem4  25473  sltres  25532  nobndlem8  25567  ax5seglem1  25771  axcontlem2  25808  axcontlem8  25814  ltflcei  26140  areacirc  26187  clsun  26221  neiin  26225  filbcmb  26332  ismtybnd  26406  grpoeqdivid  26446  ghomco  26448  rngonegrmul  26458  zerdivemp1x  26461  rngohomco  26480  rngoisoco  26488  riscer  26494  intidl  26529  isfldidl  26568  mzprename  26696  dvdsrabdioph  26760  pell14qrdivcl  26818  monotoddzz  26896  dvdsabsmod0  26947  jm2.19lem2  26951  jm2.19  26954  psgnunilem4  27288  dvconstbi  27419  stoweidlem3  27619  stoweidlem10  27626  stoweidlem19  27635  stoweidlem31  27647  stoweidlem34  27650  stoweidlem44  27660  sigaraf  27710  sigarmf  27711  f13dfv  27962  elfzmlbm  27977  elfzmlbp  27978  swrdnd  28001  swrd0swrd  28009  swrdswrd  28011  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12c  28028  swrdccat3  28029  swrdccat3a  28030  swrdccat3b  28031  usg2wlkonot  28080  usg2wotspth  28081  2spontn0vne  28084  frgra3v  28106  usg2spot2nb  28168  reccot  28215  rectan  28216  chordthmALT  28755  lubunNEW  29456  lshpnelb  29467  opnlen0  29671  lub0N  29672  glb0N  29676  opcon3b  29679  opcon2b  29680  oplecon3b  29683  opltcon3b  29687  opltcon2b  29689  oldmm1  29700  oldmm4  29703  oldmj1  29704  oldmj4  29707  cvrval2  29757  cvrcon3b  29760  leatb  29775  atcmp  29794  atcvreq0  29797  atlatle  29803  athgt  29938  3dim2  29950  islln2a  29999  lplnnleat  30024  lvolnleat  30065  4atlem10  30088  4atlem11  30091  4atlem12  30094  dalem21  30176  dalem22  30177  dalem23  30178  dalem29  30183  dalem30  30184  dalem31N  30185  dalem32  30186  dalem33  30187  dalem34  30188  dalem35  30189  dalem36  30190  dalem37  30191  dalem40  30194  dalem46  30200  dalem47  30201  dalem51  30205  dalem52  30206  dalem58  30212  dalem59  30213  pmaple  30243  paddclN  30324  pmapjoin  30334  pmapjat1  30335  elpcliN  30375  pclssN  30376  pclun2N  30381  2polcon4bN  30400  paddunN  30409  poldmj1N  30410  pmapj2N  30411  pmapocjN  30412  psubclinN  30430  paddatclN  30431  poml4N  30435  lautco  30579  ldilco  30598  ltrneq2  30630  trljat1  30648  cdlemc1  30673  cdleme10  30736  ltrnco  31201  trlcocnv  31202  trljco  31222  trljco2  31223  cdlemi1  31300  tendocnv  31504  diaord  31530  dibord  31642  dihord3  31740  dihord4  31741  dihmeetlem2N  31782  dihmeetlem4preN  31789  dochdmj1  31873  hdmap10lem  32325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator