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

Theorem 3adant1 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
3adant1  |-  ( ( th  /\  ph  /\  ps )  ->  ch )

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 957 . 2  |-  ( ( th  /\  ph  /\  ps )  ->  ( ph  /\ 
ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 16 1  |-  ( ( th  /\  ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3ad2ant2  980  3ad2ant3  981  rsp2e  2771  sbciegft  3193  reuhyp  4753  ordunel  4809  breldmg  5077  funopg  5487  fex2  5605  fvun1  5796  fnreseql  5842  ftpg  5918  mpt2eq3ia  6141  poxp  6460  smores3  6617  oaord  6792  oacan  6793  oaword  6794  omord  6813  omcan  6814  omwordri  6817  odi  6824  omass  6825  oeord  6833  oecan  6834  oewordri  6837  oeordsuc  6839  nnaord  6864  nnaordr  6865  nndi  6868  nnmass  6869  nnaword  6872  nnmord  6877  nnmwordri  6881  erov  7003  ecopovtrn  7009  ixpf  7086  mapxpen  7275  fimax2g  7355  unbnn  7365  inelfi  7425  elfiun  7437  suppr  7475  r111  7703  dif1card  7894  xpcdaen  8065  mapcdaen  8066  ackbij1lem16  8117  cff1  8140  cfflb  8141  cfsmolem  8152  fin23lem34  8228  hsmexlem2  8309  axcc3  8320  domtriomlem  8324  axdc3lem4  8335  axdc4lem  8337  axcclem  8339  konigthlem  8445  gchdomtri  8506  tskpr  8647  tskop  8648  tskuni  8660  tskun  8663  gruop  8682  gruun  8683  grudomon  8694  adderpqlem  8833  mulerpqlem  8834  addassnq  8837  mulassnq  8838  distrnq  8840  ltsonq  8848  ltanq  8850  ltmnq  8851  genpass  8888  distrlem1pr  8904  distrlem4pr  8905  ltsopr  8911  adddir  9085  axlttrn  9150  ltletr  9168  letr  9169  mul32  9235  mul31  9236  add32  9282  subsub23  9312  addsubass  9317  subcan2  9328  subsub2  9331  nppcan2  9334  sub32  9337  nnncan  9338  nnncan2  9340  pnpcan2  9343  subdi  9469  subdir  9470  receu  9669  divmul3  9685  divrec  9696  divrec2  9697  divsubdir  9712  divdiv1  9727  redivcl  9735  div2neg  9739  ltmul2  9863  lemul1  9864  lemul2  9865  lemul2a  9867  lediv1  9877  gt0div  9878  ge0div  9879  ltdivmul  9884  ledivmul  9885  ledivmulOLD  9886  ltdivmul2  9887  ledivmul2  9889  ledivmul2OLD  9890  lemuldiv  9891  ltdiv23  9903  lediv23  9904  ledivp1i  9938  ltdivp1i  9939  uzind2  10364  nn0ind  10368  fnn0ind  10371  xrltletr  10749  xrletr  10750  xrre2  10760  xrltmin  10772  xrlemin  10774  xleadd2a  10835  xleadd1  10836  xltadd2  10838  xmulasslem3  10867  xmulass  10868  xltmul2  10874  ixxdisj  10933  iooneg  11019  iccneg  11020  icoshft  11021  icoshftf1o  11022  icodisj  11024  snunioo  11025  fzen  11074  fzrev3  11113  fzoaddel2  11178  modcyc  11278  modcyc2  11279  moddi  11286  modsubdir  11287  expdiv  11432  digit2  11514  brfi1uzind  11717  ccatass  11752  swrdval  11766  ccatco  11806  shftval2  11892  mulre  11928  absdiv  12102  absdiflt  12123  absdifle  12124  abs3dif  12137  cau3  12161  ello12r  12313  elo12r  12324  geoisum1c  12659  rpnnen2lem4  12819  rpnnen2lem7  12822  dvdsmulc  12879  dvdsmulcr  12881  dvdsmultr1  12886  dvdsmultr2  12887  dvdssub2  12889  oexpneg  12913  divalgb  12926  ndvdsadd  12930  sadass  12985  modgcd  13038  dvdsgcd  13045  dvdsgcdb  13046  gcdass  13047  mulgcd  13048  absmulgcd  13049  rpmulgcd  13057  nn0seqcvgd  13063  algcvga  13072  coprmdvds  13104  coprmdvds2  13105  rpmul  13125  qnumdenbi  13138  coprimeprodsq  13185  pythagtriplem4  13195  pythagtriplem8  13199  pythagtriplem9  13200  pythagtriplem12  13202  pythagtriplem14  13204  pythagtriplem16  13206  pcpremul  13219  pcgcd  13253  vdwapval  13343  vdwapun  13344  mreiincl  13823  mreincl  13826  mremre  13831  mrcss  13843  catcisolem  14263  pleval2  14424  pospo  14432  clatl  14545  lubss  14550  lubun  14552  clatglbss  14556  ipole  14586  ipolt  14587  pslem  14640  dirtr  14683  gsumws2  14790  frmdmnd  14806  isgrpi  14833  grpsubrcan  14872  grpinvsub  14873  grpsubeq0  14877  grpnpcan  14882  divssub  15002  ghmsub  15016  symggrp  15105  lsmass  15304  efgsrel  15368  cntzcmn  15461  dvrcl  15793  unitdvcl  15794  dvrcan1  15798  subrgmre  15894  abvsubtri  15925  abvtrivd  15930  lmodvsubval2  16001  lss0cl  16025  lssintcl  16042  lssincl  16043  reslmhm2  16131  lspvadd  16170  lspsntrim  16172  islbs3  16229  rrgeq0  16352  cncrng  16724  xrsmcmn  16726  cndrng  16732  cnsrng  16737  xrs1mnd  16738  absabv  16758  unopn  16978  clsss  17120  cldmre  17144  toponmre  17159  opnssneib  17181  restabs  17231  restcls  17247  restntr  17248  hausnei2  17419  cmpsublem  17464  hausmapdom  17565  ptpjcn  17645  upxp  17657  ptrescn  17673  xkopjcn  17690  fbssfi  17871  snfil  17898  ufprim  17943  rnelfm  17987  flimrest  18017  fclsrest  18058  tmdgsum  18127  blpnfctr  18468  mscl  18493  xmscl  18494  xmsge0  18495  xmseq0  18496  restmetu  18619  ngpds  18652  unitnmn0  18706  xrsxmet  18842  metds0  18882  cncfmptc  18943  cphsqrcl  19149  cfil3i  19224  cfilres  19251  cmmbl  19431  voliunlem2  19447  itg2ub  19627  itgrecl  19691  evlsval2  19943  tdeglem3  19984  r1pid  20084  efgh  20445  eflogeq  20498  cxpadd  20572  lawcos  20660  pythag  20661  asinsinb  20739  acoscosb  20740  atantanb  20766  amgmlem  20830  lgsneg  21105  lgsne0  21119  nb3graprlem2  21463  cusgra3v  21475  cusgrasizeindslem3  21486  sizeusglecusglem2  21496  usgrnloop  21565  spthonepeq  21589  constr2spth  21602  constr2pth  21603  redwlk  21608  cyclispthon  21622  usgrcyclnl1  21629  usgrcyclnl2  21630  3v3e3cycl1  21633  constr3lem5  21637  constr3trllem2  21640  constr3pthlem2  21645  4cycl4v4e  21655  4cycl4dv4e  21657  vdgrfval  21668  gxnn0suc  21854  issubgoi  21900  ablomul  21945  imsmetlem  22184  nmoxr  22269  nmoolb  22274  blometi  22306  phpar2  22326  phpar  22327  ipasslem5  22338  hvadd32  22538  hvaddsub12  22542  hvaddsubass  22545  hvsubass  22548  hvsub32  22549  hvsubdistr1  22553  hvsubdistr2  22554  hvmulcan  22576  hvmulcan2  22577  hvsubcan  22578  his5  22590  his2sub  22596  hhssnv  22766  shlej2  22865  pjoi0  23221  hodcl  23252  hoadd32  23288  hosubdi  23313  hosubsub2  23317  hoaddsubass  23320  hosubsub4  23323  nmoplb  23412  unop  23420  hmop  23427  nmfnlb  23429  lnopmul  23472  kbass1  23621  kbass2  23622  leopmul2i  23640  leoptr  23642  cvntr  23797  mdslmd4i  23838  mdexchi  23840  atcv1  23885  sumdmdii  23920  xreceu  24170  isinftm  24253  unitdivcld  24301  logblt  24408  esummulc1  24473  hasheuni  24477  unelsiga  24519  cvmsf1o  24961  cvmscld  24962  modaddabs  25117  lediv2aALT  25119  mulcan1g  25191  mulcan2g  25192  mulsuble0b  25195  subdivcomb2  25198  gcd32  25372  fununiq  25396  trpredpo  25515  poseq  25530  wfr3g  25539  frr3g  25583  sltres  25621  nocvxmin  25648  dfrdg4  25797  brbtwn2  25846  colinearalg  25851  eleesubd  25853  axcgrrflx  25855  axcgrtr  25856  axsegcon  25868  ax5seglem1  25869  ax5seglem2  25870  ax5seglem4  25873  axbtwnid  25880  axlowdimlem14  25896  axlowdim  25902  axcontlem5  25909  axcontlem7  25911  brcolinear  25995  colinearex  25996  cnambfre  26257  ftc1anclem4  26285  nn0prpwlem  26327  clsun  26333  fnemeet1  26397  fnemeet2  26398  fnejoin1  26399  fnejoin2  26400  eltail  26405  cocanfo  26421  f1ocan1fv  26430  metf1o  26463  ismtybnd  26518  ghomco  26560  isdrngo2  26576  inidl  26642  igenmin  26676  mapco2g  26771  mzpcompact2lem  26810  eqrabdioph  26838  lerabdioph  26867  eluzrabdioph  26868  ltrabdioph  26870  nerabdioph  26871  dvdsrabdioph  26872  reglogcl  26955  rmxyadd  26986  rmyabs  27025  congadd  27033  congabseq  27041  rmydioph  27087  uvcresum  27221  lindfmm  27276  lindsmm  27277  symggen  27390  mendrng  27479  mendlmod  27480  dvconstbi  27530  fmul01  27688  stoweidlem60  27787  stowei  27791  sigarls  27825  f13dfv  28087  2ffzeq  28132  fzoopth  28150  flltdivnn0lt  28158  ltdifltdiv  28159  modsubmodmod  28167  modaddmulmod  28169  swrdnd  28204  swrdvalodmlem1  28209  swrdvalodm2  28210  swrd0swrd  28219  swrdswrdlem  28220  swrdccatin12lem3a  28230  swrdccatin12lem3b  28231  prmgt1  28245  modprm0  28250  cshweqdif2  28292  iswlkg  28326  usg2wlkeq  28330  usgra2pthspth  28331  wwlknimp  28357  wlkiswwlk1  28360  wlkiswwlk2lem4  28364  wlkiswwlk2lem6  28366  el2spthonot  28390  el2spthonot0  28391  usg2wlkonot  28403  rusgrargra  28433  frgra3v  28454  3vfriswmgra  28457  frgrawopreg  28500  frg2woteu  28506  frgregordn0  28521  bnj545  29328  bnj594  29345  bnj1311  29455  lubunNEW  29833  cmtvalN  30071  cvrval  30129  pmapmeet  30632  paddval  30657  paddssat  30673  elpcliN  30752  pclssN  30753  pclunN  30757  paddunN  30786  poldmj1N  30787  tendoplcl2  31637  tendoplcl  31640  dihmeet  32203
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator