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  2353  eupickbOLD  2354  vtoclegft  3150  eqeu  3237  funopg  5559  fnco  5628  dff1o2  5755  fnimapr  5865  fvmptt  5899  fnreseql  5923  f1elima  6086  f1ocnvfvb  6096  oprssov  6343  ordunel  6549  poxp  6795  smoiso  6934  oaord  7097  oaword  7099  omcan  7119  omwordri  7122  odi  7129  omeulem1  7132  oeord  7138  oecan  7139  oewordri  7142  oeordsuc  7144  nnaord  7169  nnaordr  7170  nndi  7173  nnaword  7177  nnmwordri  7186  erov  7308  ecopovtrn  7314  xpdom3  7520  mapxpen  7588  findcard  7663  indexfi  7731  suppr  7830  r111  8094  tcrank  8203  acndom  8333  infdif2  8491  infxpdom  8492  cfeq0  8537  cfsuc  8538  cfflb  8540  cflim2  8544  cfsmolem  8551  axcc3  8719  domtriomlem  8723  axdc3lem2  8732  axdc3lem4  8734  axdc4lem  8736  axcclem  8738  pwcfsdom  8859  tsktrss  9040  tsksuc  9041  tskuni  9062  adderpqlem  9235  mulerpqlem  9236  mulcanenq  9241  distrnq  9242  ltsonq  9250  ltanq  9252  ltmnq  9253  distrlem1pr  9306  distrlem5pr  9308  ltsopr  9313  ltsosr  9373  ltasr  9379  adddir  9489  axlttrn  9559  letr  9580  ltneOLD  9584  nnncan1  9757  npncan3  9759  pnpcan2  9761  subdi  9890  subdir  9891  mulcan1g  10101  mulcan2g  10102  divmul  10109  div23  10125  div13  10127  divsubdir  10139  divcan7  10152  ltmul2  10292  lemul1  10293  lemul2  10294  lemul2a  10296  lediv1  10306  ltmuldiv2  10315  lemuldiv  10323  lemuldiv2  10324  ltdiv2  10329  lediv2  10334  infmrlb  10423  nndivtr  10475  bndndx  10690  nn0n0n1ge2  10755  fnn0ind  10853  lbzbi  11055  xrletr  11244  qsqueeze  11283  xleadd2a  11329  xleadd1  11330  xltadd2  11332  xltmul2  11368  supxrbnd  11403  iooneg  11523  iccneg  11524  icoshft  11525  icoshftf1o  11526  fzen  11585  uzsubsubfz  11589  fz0fzdiffz0  11607  elfzmlbm  11608  elfzmlbp  11609  fzrevral2  11663  fzshftral  11665  elfzo  11673  fzoaddel2  11716  fzosubel2  11718  ssfzo12bi  11740  fzonfzoufzol  11746  flltdivnn0lt  11795  modmulnn  11843  modcyc  11861  modaddabs  11864  modaddmod  11865  modadd2mod  11867  modsubmod  11875  modsubmodmod  11876  modaddmodup  11880  modmulmod  11882  moddi  11884  modsubdir  11885  uzindi  11921  axdc4uzlem  11922  expneg2  11992  expdiv  12032  expubnd  12042  bernneq2  12109  hashinfxadd  12267  brfi1indlem  12337  ccatsymb  12400  ccatfv0  12401  ccats1val2  12426  swrdnd  12445  swrdvalodm2  12452  2swrd1eqwrdeq  12467  swrdswrd  12473  wrd2ind  12491  swrdccatin1  12493  swrdccatin12lem2b  12496  swrdccatin2  12497  swrdccatin12lem2  12499  swrdccatin12lem3  12500  swrdccat  12503  swrdccat3a  12504  swrdccat3blem  12505  repswswrd  12541  repswccat  12542  cshwidxmod  12559  2cshw  12566  3cshw  12571  ccatco  12582  cshco  12583  swrdco  12584  lswco  12585  swrds2  12664  2swrd2eqwrdeq  12672  shftuz  12677  shftval2  12683  abs3dif  12938  sin02gt0  13595  dvdsval2  13657  dvdscmul  13678  dvdsmulc  13679  dvdscmulr  13680  dvdsmulcr  13681  divalglem8  13723  ndvdssub  13730  rpmulgcd  13858  isprm3  13891  coprmdvds  13907  modprm0  13992  coprimeprodsq  13995  pythagtriplem12  14012  pythagtriplem14  14014  pcprendvds  14026  pcmul  14037  pcdiv  14038  pcqcl  14042  pcqdiv  14043  pcdvdsb  14054  pcgcd  14063  vdwnnlem1  14175  hashbcss  14184  cshwshashlem1  14241  fvsetsid  14318  mrcss  14674  mrcsscl  14678  mrcun  14680  cofulid  14920  catcisolem  15094  latleeqj1  15353  lubun  15413  clatleglb  15416  pslem  15496  dirtr  15526  pwspjmhm  15616  gsumccat  15639  grpinvid1  15706  grpinvid2  15707  grpinvadd  15724  grpsubf  15725  grpsubrcan  15727  grpinvsub  15728  grpsubeq0  15732  grppncan  15736  grpnpcan  15737  mulgnn0p1  15758  subgsubcl  15812  subgsub  15813  eqglact  15852  divssub  15861  ghmsub  15875  psgnunilem4  16123  oddvds2  16189  odsubdvds  16192  gexnnod  16209  slwn0  16236  gsumsn  16572  gsumdixpOLD  16824  gsumdixp  16825  dvrcl  16902  unitdvcl  16903  dvrcan1  16907  dvrcan3  16908  dvreq1  16909  subrgdv  17006  abvsubtri  17044  idsrngd  17071  lmodvsubval2  17124  lsmcl  17288  lsmsp2  17292  lspsntrim  17303  lidldvgen  17461  evlslem4OLD  17715  evlslem4  17716  mpfsubrg  17743  ply1tmcl  17850  chrcong  18086  zndvds  18108  zntoslem  18115  ocvsscon  18226  obselocv  18279  frlmphl  18332  mamudm  18414  mamufacex  18415  submabas  18517  mdetdiaglem  18537  mdetralt2  18548  mdetero  18549  mdetunilem2  18552  mdetunilem6  18556  m2detleiblem7  18566  maducoeval2  18579  gsummatr01lem3  18596  gsummatr01  18598  smadiadetglem2  18611  cramerlem1  18626  istps3OLD  18660  ntrin  18798  elnei  18848  neindisj2  18860  ordtopn3  18933  ordtcld3  18936  leordtval2  18949  lecldbas  18956  cnrest2  19023  cmpsublem  19135  ptrescn  19345  xkococn  19366  kqfeq  19430  snfbas  19572  neifil  19586  fclsrest  19730  utopsnnei  19957  neipcfilu  20004  psmetsym  20019  psmetge0  20021  xmetge0  20052  xmetsym  20055  metusttoOLD  20265  metustto  20266  metustblOLD  20288  metustbl  20289  restmetu  20295  nm2dif  20349  nmtri  20350  cnmet  20484  cnmpt2pc  20633  iihalf1  20636  iihalf2  20638  icoopnst  20644  iocopnst  20645  cphsqrcl3  20839  cph2ass  20864  caublcls  20952  bcthlem3  20970  bcthlem4  20971  srabn  21005  rrxmet  21040  iblconst  21429  tdeglem3  21662  mdegmullem  21683  dvdsq1p  21766  coeid3  21842  aannenlem2  21929  pserdvlem2  22027  tanord1  22127  efgh  22131  cxpef  22244  recxpcl  22254  lawcos  22346  pythag  22347  isosctrlem1  22350  isosctrlem2  22351  ax5seglem1  23327  axcontlem2  23364  axcontlem8  23370  fiusgraedgfi  23473  nbgraf1olem3  23505  nb3graprlem2  23513  cusgra3v  23525  cusgrasizeindslem3  23536  cusgrasizeinds  23537  iswlkon  23583  istrlon  23593  2trllemE  23605  usgrnloop  23615  ispthon  23628  isspthon  23635  usgrcyclnl2  23680  3v3e3cycl1  23683  constr3lem4  23686  constr3lem5  23687  constr3lem6  23688  constr3trllem2  23690  constr3trllem3  23691  4cycl4dv  23706  isgrpo  23836  grpoinvid1  23870  grpoinvid2  23871  grpoasscan1  23877  grpoasscan2  23878  grpoinvop  23881  grpodivinv  23884  grpoinvdiv  23885  grpodivf  23886  grpopncan  23891  grponpcan  23892  grpopnpcan2  23893  gxid  23913  resgrprn  23920  ablonncan  23934  zerdivemp1  24074  vcnegsubdi2  24106  vcsub4  24107  nvmval  24175  nvmval2  24176  nvmfval  24177  nvmul0or  24185  nvsubadd  24188  nvpncan2  24189  nvaddsub4  24194  nvnncan  24196  nvmeq0  24197  nvdif  24206  nvpi  24207  nvmtri  24212  nvabs  24214  imsmetlem  24234  ipval2lem3  24253  ipval2  24255  4ipval2  24256  ipval3  24257  ipval2lem6  24259  nmooge0  24320  blometi  24356  hvaddsub12  24593  hvsubdistr1  24604  hvsubdistr2  24605  hvaddcan2  24626  hvmulcan  24627  hvmulcan2  24628  hvsubcan  24629  hvsubcan2  24630  his7  24645  his2sub  24647  his2sub2  24648  norm3dif2  24706  shsubcl  24776  hhssnv  24818  shlej2  24917  fh2  25175  cm2j  25176  pjoi0  25273  hodcl  25304  hosubdi  25365  unopf1o  25473  unopadj  25476  adj2  25491  braadd  25502  bramul  25503  lnopaddmuli  25530  lnopsubmuli  25532  homco2  25534  lnfnaddmuli  25602  adjlnop  25643  leopmul  25691  leoptr  25694  pjimai  25733  atcv1  25937  atexch  25938  atcvatlem  25942  divnumden2  26233  xdivmul  26246  gsumsnf  26390  resvsca  26444  relogbcl  26607  logblt  26611  hasheuni  26680  difelsiga  26722  cndprobin  26962  bayesth  26967  sgn3da  27069  ghomf1olem  27458  lediv2aALT  27467  subdivcomb1  27529  fununiq  27726  dfrdg2  27754  wfrlem4  27872  sltres  27950  nobndlem8  27985  ltflcei  28568  ftc1anclem4  28619  areacirc  28638  clsun  28672  neiin  28676  filbcmb  28783  ismtybnd  28855  grpoeqdivid  28895  ghomco  28897  rngonegrmul  28907  zerdivemp1x  28910  rngohomco  28929  rngoisoco  28937  riscer  28943  intidl  28978  isfldidl  29017  mzprename  29235  dvdsrabdioph  29297  pell14qrdivcl  29355  monotoddzz  29433  dvdsabsmod0  29484  jm2.19lem2  29488  jm2.19  29491  dvconstbi  29757  stoweidlem3  29947  stoweidlem10  29954  stoweidlem19  29963  stoweidlem31  29975  stoweidlem34  29978  stoweidlem44  29988  sigaraf  30038  sigarmf  30039  f13dfv  30296  subsubelfzo0  30359  elfzom1p1elfzo  30364  elfzom1elp1fzo  30367  modfsummods  30393  mulmoddvds  30395  usg2wlkonot  30551  usg2wotspth  30552  2spontn0vne  30555  clwwlkgt0  30583  clwwlknndef  30585  clwlkisclwwlklem2a4  30595  clwlkisclwwlklem2a  30596  clwwlkel  30604  clwwlkext2edg  30613  clwwisshclwwlem1  30618  clwwnisshclwwn  30622  clwwlknfi  30626  erclwwlktr0  30628  erclwwlktr  30634  scshwfzeqfzo  30641  erclwwlkntr  30650  clwlkfclwwlk  30666  clwlkfoclwwlk  30667  nbhashnn0  30681  nbhashuvtx  30683  usgrauvtxvdbi  30685  wwlkextproplem3  30711  rusgra0edg  30722  frgra3v  30743  usg2spot2nb  30807  numclwlk3lem3  30815  extwwlkfablem2  30820  numclwwlkovf2ex  30828  numclwwlkovgelim  30831  numclwwlk4  30852  numclwwlk5lem  30853  numclwwlk5  30854  numclwwlk6  30855  numclwwlk7  30856  xpprsng  30868  nn0sumltlt  30891  grpsubadd0sub  30915  invginvrid  30921  ply1sclrmsm  30983  eqcoe1ply1eq  30989  gsummoncoe1  30997  lply1binomsc  31011  linccl  31081  lincvalpr  31085  lincresunit3lem1  31146  lincresunit3  31148  mply1topmatcl  31293  mp2pm2mplem4  31297  reccot  31422  rectan  31423  chordthmALT  32002  isosctrlem1ALT  32003  lshpnelb  32968  opnlen0  33172  opcon3b  33180  opcon2b  33181  oplecon3b  33184  opltcon3b  33188  opltcon2b  33190  oldmm1  33201  oldmm4  33204  oldmj1  33205  oldmj4  33208  cvrval2  33258  cvrcon3b  33261  leatb  33276  atcmp  33295  atcvreq0  33298  atlatle  33304  athgt  33439  3dim2  33451  islln2a  33500  lplnnleat  33525  lvolnleat  33566  4atlem10  33589  4atlem11  33592  4atlem12  33595  dalem21  33677  dalem22  33678  dalem23  33679  dalem29  33684  dalem30  33685  dalem31N  33686  dalem32  33687  dalem33  33688  dalem34  33689  dalem35  33690  dalem36  33691  dalem37  33692  dalem40  33695  dalem46  33701  dalem47  33702  dalem51  33706  dalem52  33707  dalem58  33713  dalem59  33714  pmaple  33744  paddclN  33825  pmapjoin  33835  pmapjat1  33836  elpcliN  33876  pclssN  33877  pclun2N  33882  2polcon4bN  33901  paddunN  33910  poldmj1N  33911  pmapj2N  33912  pmapocjN  33913  psubclinN  33931  paddatclN  33932  poml4N  33936  lautco  34080  ldilco  34099  ltrneq2  34131  trljat1  34149  cdlemc1  34174  cdleme10  34237  ltrnco  34702  trlcocnv  34703  trljco  34723  trljco2  34724  cdlemi1  34801  tendocnv  35005  diaord  35031  dibord  35143  dihord3  35241  dihord4  35242  dihmeetlem2N  35283  dihmeetlem4preN  35290  dochdmj1  35374  hdmap10lem  35826
  Copyright terms: Public domain W3C validator