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

Theorem 3adant2 1007
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 986 . 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 965
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 967
This theorem is referenced by:  3ad2ant1  1009  eupickb  2342  eupickbOLD  2343  vtoclegft  3039  eqeu  3125  funopg  5445  fnco  5514  dff1o2  5641  fnimapr  5750  fvmptt  5784  fnreseql  5808  f1elima  5971  f1ocnvfvb  5981  oprssov  6227  ordunel  6433  poxp  6679  smoiso  6815  oaord  6978  oaword  6980  omcan  7000  omwordri  7003  odi  7010  omeulem1  7013  oeord  7019  oecan  7020  oewordri  7023  oeordsuc  7025  nnaord  7050  nnaordr  7051  nndi  7054  nnaword  7058  nnmwordri  7067  erov  7189  ecopovtrn  7195  xpdom3  7401  mapxpen  7469  findcard  7543  indexfi  7611  suppr  7710  r111  7974  tcrank  8083  acndom  8213  infdif2  8371  infxpdom  8372  cfeq0  8417  cfsuc  8418  cfflb  8420  cflim2  8424  cfsmolem  8431  axcc3  8599  domtriomlem  8603  axdc3lem2  8612  axdc3lem4  8614  axdc4lem  8616  axcclem  8618  pwcfsdom  8739  tsktrss  8920  tsksuc  8921  tskuni  8942  adderpqlem  9115  mulerpqlem  9116  mulcanenq  9121  distrnq  9122  ltsonq  9130  ltanq  9132  ltmnq  9133  distrlem1pr  9186  distrlem5pr  9188  ltsopr  9193  ltsosr  9253  ltasr  9259  adddir  9369  axlttrn  9439  letr  9460  ltneOLD  9464  nnncan1  9637  npncan3  9639  pnpcan2  9641  subdi  9770  subdir  9771  mulcan1g  9981  mulcan2g  9982  divmul  9989  div23  10005  div13  10007  divsubdir  10019  divcan7  10032  ltmul2  10172  lemul1  10173  lemul2  10174  lemul2a  10176  lediv1  10186  ltmuldiv2  10195  lemuldiv  10203  lemuldiv2  10204  ltdiv2  10209  lediv2  10214  infmrlb  10303  nndivtr  10355  bndndx  10570  nn0n0n1ge2  10635  fnn0ind  10733  lbzbi  10935  xrletr  11124  qsqueeze  11163  xleadd2a  11209  xleadd1  11210  xltadd2  11212  xltmul2  11248  supxrbnd  11283  iooneg  11397  iccneg  11398  icoshft  11399  icoshftf1o  11400  fzen  11459  uzsubsubfz  11463  fz0fzdiffz0  11481  elfzmlbm  11482  elfzmlbp  11483  fzrevral2  11537  fzshftral  11539  elfzo  11547  fzoaddel2  11590  fzosubel2  11592  ssfzo12bi  11614  fzonfzoufzol  11620  flltdivnn0lt  11669  modmulnn  11717  modcyc  11735  modaddabs  11738  modaddmod  11739  modadd2mod  11741  modsubmod  11749  modsubmodmod  11750  modaddmodup  11754  modmulmod  11756  moddi  11758  modsubdir  11759  uzindi  11795  axdc4uzlem  11796  expneg2  11866  expdiv  11906  expubnd  11916  bernneq2  11983  hashinfxadd  12140  brfi1indlem  12210  ccatsymb  12273  ccatfv0  12274  ccats1val2  12299  swrdnd  12318  swrdvalodm2  12325  2swrd1eqwrdeq  12340  swrdswrd  12346  wrd2ind  12364  swrdccatin1  12366  swrdccatin12lem2b  12369  swrdccatin2  12370  swrdccatin12lem2  12372  swrdccatin12lem3  12373  swrdccat  12376  swrdccat3a  12377  swrdccat3blem  12378  repswswrd  12414  repswccat  12415  cshwidxmod  12432  2cshw  12439  3cshw  12444  ccatco  12455  cshco  12456  swrdco  12457  lswco  12458  swrds2  12537  2swrd2eqwrdeq  12545  shftuz  12550  shftval2  12556  abs3dif  12811  sin02gt0  13468  dvdsval2  13530  dvdscmul  13551  dvdsmulc  13552  dvdscmulr  13553  dvdsmulcr  13554  divalglem8  13596  ndvdssub  13603  rpmulgcd  13731  isprm3  13764  coprmdvds  13780  modprm0  13865  coprimeprodsq  13868  pythagtriplem12  13885  pythagtriplem14  13887  pcprendvds  13899  pcmul  13910  pcdiv  13911  pcqcl  13915  pcqdiv  13916  pcdvdsb  13927  pcgcd  13936  vdwnnlem1  14048  hashbcss  14057  cshwshashlem1  14114  fvsetsid  14191  mrcss  14546  mrcsscl  14550  mrcun  14552  cofulid  14792  catcisolem  14966  latleeqj1  15225  lubun  15285  clatleglb  15288  pslem  15368  dirtr  15398  pwspjmhm  15487  gsumccat  15510  grpinvid1  15577  grpinvid2  15578  grpinvadd  15595  grpsubf  15596  grpsubrcan  15598  grpinvsub  15599  grpsubeq0  15603  grppncan  15607  grpnpcan  15608  mulgnn0p1  15629  subgsubcl  15683  subgsub  15684  eqglact  15723  divssub  15732  ghmsub  15746  psgnunilem4  15994  oddvds2  16058  odsubdvds  16061  gexnnod  16078  slwn0  16105  gsumsn  16439  gsumdixpOLD  16688  gsumdixp  16689  dvrcl  16766  unitdvcl  16767  dvrcan1  16771  dvrcan3  16772  dvreq1  16773  subrgdv  16860  abvsubtri  16898  idsrngd  16925  lmodvsubval2  16978  lsmcl  17141  lsmsp2  17145  lspsntrim  17156  lidldvgen  17314  evlslem4OLD  17565  evlslem4  17566  mpfsubrg  17593  chrcong  17935  zndvds  17957  zntoslem  17964  ocvsscon  18075  obselocv  18128  frlmphl  18181  mamudm  18263  mamufacex  18264  submabas  18364  mdetralt2  18390  mdetero  18391  mdetunilem2  18394  mdetunilem6  18398  m2detleiblem7  18408  maducoeval2  18421  gsummatr01lem3  18438  gsummatr01  18440  smadiadetglem2  18453  cramerlem1  18468  istps3OLD  18502  ntrin  18640  elnei  18690  neindisj2  18702  ordtopn3  18775  ordtcld3  18778  leordtval2  18791  lecldbas  18798  cnrest2  18865  cmpsublem  18977  ptrescn  19187  xkococn  19208  kqfeq  19272  snfbas  19414  neifil  19428  fclsrest  19572  utopsnnei  19799  neipcfilu  19846  psmetsym  19861  psmetge0  19863  xmetge0  19894  xmetsym  19897  metusttoOLD  20107  metustto  20108  metustblOLD  20130  metustbl  20131  restmetu  20137  nm2dif  20191  nmtri  20192  cnmet  20326  cnmpt2pc  20475  iihalf1  20478  iihalf2  20480  icoopnst  20486  iocopnst  20487  cphsqrcl3  20681  cph2ass  20706  caublcls  20794  bcthlem3  20812  bcthlem4  20813  srabn  20847  rrxmet  20882  iblconst  21270  tdeglem3  21503  mdegmullem  21524  dvdsq1p  21607  coeid3  21683  aannenlem2  21770  pserdvlem2  21868  tanord1  21968  efgh  21972  cxpef  22085  recxpcl  22095  lawcos  22187  pythag  22188  isosctrlem1  22191  isosctrlem2  22192  ax5seglem1  23125  axcontlem2  23162  axcontlem8  23168  fiusgraedgfi  23271  nbgraf1olem3  23303  nb3graprlem2  23311  cusgra3v  23323  cusgrasizeindslem3  23334  cusgrasizeinds  23335  iswlkon  23381  istrlon  23391  2trllemE  23403  usgrnloop  23413  ispthon  23426  isspthon  23433  usgrcyclnl2  23478  3v3e3cycl1  23481  constr3lem4  23484  constr3lem5  23485  constr3lem6  23486  constr3trllem2  23488  constr3trllem3  23489  4cycl4dv  23504  isgrpo  23634  grpoinvid1  23668  grpoinvid2  23669  grpoasscan1  23675  grpoasscan2  23676  grpoinvop  23679  grpodivinv  23682  grpoinvdiv  23683  grpodivf  23684  grpopncan  23689  grponpcan  23690  grpopnpcan2  23691  gxid  23711  resgrprn  23718  ablonncan  23732  zerdivemp1  23872  vcnegsubdi2  23904  vcsub4  23905  nvmval  23973  nvmval2  23974  nvmfval  23975  nvmul0or  23983  nvsubadd  23986  nvpncan2  23987  nvaddsub4  23992  nvnncan  23994  nvmeq0  23995  nvdif  24004  nvpi  24005  nvmtri  24010  nvabs  24012  imsmetlem  24032  ipval2lem3  24051  ipval2  24053  4ipval2  24054  ipval3  24055  ipval2lem6  24057  nmooge0  24118  blometi  24154  hvaddsub12  24391  hvsubdistr1  24402  hvsubdistr2  24403  hvaddcan2  24424  hvmulcan  24425  hvmulcan2  24426  hvsubcan  24427  hvsubcan2  24428  his7  24443  his2sub  24445  his2sub2  24446  norm3dif2  24504  shsubcl  24574  hhssnv  24616  shlej2  24715  fh2  24973  cm2j  24974  pjoi0  25071  hodcl  25102  hosubdi  25163  unopf1o  25271  unopadj  25274  adj2  25289  braadd  25300  bramul  25301  lnopaddmuli  25328  lnopsubmuli  25330  homco2  25332  lnfnaddmuli  25400  adjlnop  25441  leopmul  25489  leoptr  25492  pjimai  25531  atcv1  25735  atexch  25736  atcvatlem  25740  divnumden2  26038  xdivmul  26051  gsumsnf  26195  resvsca  26250  relogbcl  26413  logblt  26417  hasheuni  26486  difelsiga  26528  cndprobin  26769  bayesth  26774  sgn3da  26876  ghomf1olem  27264  lediv2aALT  27273  subdivcomb1  27335  fununiq  27532  dfrdg2  27560  wfrlem4  27678  sltres  27756  nobndlem8  27791  ltflcei  28372  ftc1anclem4  28423  areacirc  28442  clsun  28476  neiin  28480  filbcmb  28587  ismtybnd  28659  grpoeqdivid  28699  ghomco  28701  rngonegrmul  28711  zerdivemp1x  28714  rngohomco  28733  rngoisoco  28741  riscer  28747  intidl  28782  isfldidl  28821  mzprename  29039  dvdsrabdioph  29101  pell14qrdivcl  29159  monotoddzz  29237  dvdsabsmod0  29288  jm2.19lem2  29292  jm2.19  29295  dvconstbi  29561  stoweidlem3  29751  stoweidlem10  29758  stoweidlem19  29767  stoweidlem31  29779  stoweidlem34  29782  stoweidlem44  29792  sigaraf  29842  sigarmf  29843  f13dfv  30100  subsubelfzo0  30163  elfzom1p1elfzo  30168  elfzom1elp1fzo  30171  modfsummods  30197  mulmoddvds  30199  usg2wlkonot  30355  usg2wotspth  30356  2spontn0vne  30359  clwwlkgt0  30387  clwwlknndef  30389  clwlkisclwwlklem2a4  30399  clwlkisclwwlklem2a  30400  clwwlkel  30408  clwwlkext2edg  30417  clwwisshclwwlem1  30422  clwwnisshclwwn  30426  clwwlknfi  30430  erclwwlktr0  30432  erclwwlktr  30438  scshwfzeqfzo  30445  erclwwlkntr  30454  clwlkfclwwlk  30470  clwlkfoclwwlk  30471  nbhashnn0  30485  nbhashuvtx  30487  usgrauvtxvdbi  30489  wwlkextproplem3  30515  rusgra0edg  30526  frgra3v  30547  usg2spot2nb  30611  numclwlk3lem3  30619  extwwlkfablem2  30624  numclwwlkovf2ex  30632  numclwwlkovgelim  30635  numclwwlk4  30656  numclwwlk5lem  30657  numclwwlk5  30658  numclwwlk6  30659  numclwwlk7  30660  xpprsng  30671  invginvrid  30723  ply1sclrmsm  30768  lply1binomsc  30775  mdetdiaglem  30824  linccl  30837  lincvalpr  30841  lincresunit3lem1  30902  lincresunit3  30904  reccot  30982  rectan  30983  chordthmALT  31556  isosctrlem1ALT  31557  lshpnelb  32469  opnlen0  32673  opcon3b  32681  opcon2b  32682  oplecon3b  32685  opltcon3b  32689  opltcon2b  32691  oldmm1  32702  oldmm4  32705  oldmj1  32706  oldmj4  32709  cvrval2  32759  cvrcon3b  32762  leatb  32777  atcmp  32796  atcvreq0  32799  atlatle  32805  athgt  32940  3dim2  32952  islln2a  33001  lplnnleat  33026  lvolnleat  33067  4atlem10  33090  4atlem11  33093  4atlem12  33096  dalem21  33178  dalem22  33179  dalem23  33180  dalem29  33185  dalem30  33186  dalem31N  33187  dalem32  33188  dalem33  33189  dalem34  33190  dalem35  33191  dalem36  33192  dalem37  33193  dalem40  33196  dalem46  33202  dalem47  33203  dalem51  33207  dalem52  33208  dalem58  33214  dalem59  33215  pmaple  33245  paddclN  33326  pmapjoin  33336  pmapjat1  33337  elpcliN  33377  pclssN  33378  pclun2N  33383  2polcon4bN  33402  paddunN  33411  poldmj1N  33412  pmapj2N  33413  pmapocjN  33414  psubclinN  33432  paddatclN  33433  poml4N  33437  lautco  33581  ldilco  33600  ltrneq2  33632  trljat1  33650  cdlemc1  33675  cdleme10  33738  ltrnco  34203  trlcocnv  34204  trljco  34224  trljco2  34225  cdlemi1  34302  tendocnv  34506  diaord  34532  dibord  34644  dihord3  34742  dihord4  34743  dihmeetlem2N  34784  dihmeetlem4preN  34791  dochdmj1  34875  hdmap10lem  35327
  Copyright terms: Public domain W3C validator