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

Theorem 3adant1 973
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 954 . 2  |-  ( ( th  /\  ph  /\  ps )  ->  ( ph  /\ 
ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 15 1  |-  ( ( th  /\  ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ad2ant2  977  3ad2ant3  978  rsp2e  2606  sbciegft  3021  reuhyp  4562  ordunel  4618  breldmg  4884  funopg  5286  fex2  5401  fvun1  5590  fnreseql  5635  mpt2eq3ia  5913  poxp  6227  smores3  6370  oaord  6545  oacan  6546  oaword  6547  omord  6566  omcan  6567  omwordri  6570  odi  6577  omass  6578  oeord  6586  oecan  6587  oewordri  6590  oeordsuc  6592  nnaord  6617  nnaordr  6618  nndi  6621  nnmass  6622  nnaword  6625  nnmord  6630  nnmwordri  6634  erov  6755  ecopovtrn  6761  ixpf  6838  mapxpen  7027  fimax2g  7103  unbnn  7113  elfiun  7183  suppr  7219  r111  7447  dif1card  7638  xpcdaen  7809  mapcdaen  7810  ackbij1lem16  7861  cff1  7884  cfflb  7885  cfsmolem  7896  fin23lem34  7972  hsmexlem2  8053  axcc3  8064  domtriomlem  8068  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  konigthlem  8190  gchdomtri  8251  tskpr  8392  tskop  8393  tskuni  8405  tskun  8408  gruop  8427  gruun  8428  grudomon  8439  adderpqlem  8578  mulerpqlem  8579  addassnq  8582  mulassnq  8583  distrnq  8585  ltsonq  8593  ltanq  8595  ltmnq  8596  genpass  8633  distrlem1pr  8649  distrlem4pr  8650  ltsopr  8656  adddir  8830  axlttrn  8895  ltletr  8913  letr  8914  mul32  8979  mul31  8980  add32  9026  subsub23  9056  addsubass  9061  subcan2  9072  subsub2  9075  nppcan2  9078  sub32  9081  nnncan  9082  nnncan2  9084  pnpcan2  9087  subdi  9213  subdir  9214  receu  9413  divmul3  9429  divrec  9440  divrec2  9441  divsubdir  9456  divdiv1  9471  redivcl  9479  div2neg  9483  ltmul2  9607  lemul1  9608  lemul2  9609  lemul2a  9611  lediv1  9621  gt0div  9622  ge0div  9623  ltdivmul  9628  ledivmul  9629  ledivmulOLD  9630  ltdivmul2  9631  ledivmul2  9633  ledivmul2OLD  9634  lemuldiv  9635  ltdiv23  9647  lediv23  9648  ledivp1i  9682  ltdivp1i  9683  uzind2  10104  nn0ind  10108  fnn0ind  10111  xrltletr  10488  xrletr  10489  xrre2  10499  xrltmin  10511  xrlemin  10513  xleadd2a  10574  xleadd1  10575  xltadd2  10577  xmulasslem3  10606  xmulass  10607  xltmul2  10613  ixxdisj  10671  iooneg  10756  iccneg  10757  icoshft  10758  icoshftf1o  10759  icodisj  10761  snunioo  10762  fzen  10811  fzrev3  10849  fzoaddel2  10907  modcyc  10999  modcyc2  11000  moddi  11007  modsubdir  11008  expdiv  11152  digit2  11234  ccatass  11436  swrdval  11450  ccatco  11490  shftval2  11570  mulre  11606  absdiv  11780  absdiflt  11801  absdifle  11802  abs3dif  11815  cau3  11839  ello12r  11991  elo12r  12002  geoisum1c  12336  rpnnen2lem4  12496  rpnnen2lem7  12499  dvdsmulc  12556  dvdsmulcr  12558  dvdsmultr1  12563  dvdsmultr2  12564  dvdssub2  12566  oexpneg  12590  divalgb  12603  ndvdsadd  12607  sadass  12662  modgcd  12715  dvdsgcd  12722  dvdsgcdb  12723  gcdass  12724  mulgcd  12725  absmulgcd  12726  rpmulgcd  12734  nn0seqcvgd  12740  algcvga  12749  coprmdvds  12781  coprmdvds2  12782  rpmul  12802  qnumdenbi  12815  coprimeprodsq  12862  pythagtriplem4  12872  pythagtriplem8  12876  pythagtriplem9  12877  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem16  12883  pcpremul  12896  pcgcd  12930  vdwapval  13020  vdwapun  13021  mreiincl  13498  mreincl  13501  mremre  13506  mrcss  13518  catcisolem  13938  pleval2  14099  pospo  14107  clatl  14220  lubss  14225  lubun  14227  clatglbss  14231  ipole  14261  ipolt  14262  pslem  14315  dirtr  14358  gsumws2  14465  frmdmnd  14481  isgrpi  14508  grpsubrcan  14547  grpinvsub  14548  grpsubeq0  14552  grpnpcan  14557  divssub  14677  ghmsub  14691  symggrp  14780  lsmass  14979  efgsrel  15043  cntzcmn  15136  dvrcl  15468  unitdvcl  15469  dvrcan1  15473  subrgmre  15569  abvsubtri  15600  abvtrivd  15605  lmodvsubval2  15680  lss0cl  15704  lssintcl  15721  lssincl  15722  reslmhm2  15810  lspvadd  15849  lspsntrim  15851  islbs3  15908  rrgeq0  16031  cncrng  16395  xrsmcmn  16397  cndrng  16403  cnsrng  16408  xrs1mnd  16409  absabv  16429  unopn  16649  clsss  16791  cldmre  16815  toponmre  16830  opnssneib  16852  restabs  16896  restcls  16911  restntr  16912  hausnei2  17081  cmpsublem  17126  hausmapdom  17226  ptpjcn  17305  upxp  17317  ptrescn  17333  xkopjcn  17350  fbssfi  17532  snfil  17559  ufprim  17604  rnelfm  17648  flimrest  17678  fclsrest  17719  tmdgsum  17778  blpnfctr  17982  mscl  18007  xmscl  18008  xmsge0  18009  xmseq0  18010  ngpds  18125  unitnmn0  18179  xrsxmet  18315  metds0  18354  cncfmptc  18415  cphsqrcl  18620  cfil3i  18695  cfilres  18722  cmmbl  18892  voliunlem2  18908  itg2ub  19088  itgrecl  19152  evlsval2  19404  tdeglem3  19445  r1pid  19545  efgh  19903  eflogeq  19955  cxpadd  20026  lawcos  20114  pythag  20115  asinsinb  20193  acoscosb  20194  atantanb  20220  amgmlem  20284  lgsneg  20558  lgsne0  20572  gxnn0suc  20931  issubgoi  20977  ablomul  21022  imsmetlem  21259  nmoxr  21344  nmoolb  21349  blometi  21381  phpar2  21401  phpar  21402  ipasslem5  21413  hvadd32  21613  hvaddsub12  21617  hvaddsubass  21620  hvsubass  21623  hvsub32  21624  hvsubdistr1  21628  hvsubdistr2  21629  hvmulcan  21651  hvmulcan2  21652  hvsubcan  21653  his5  21665  his2sub  21671  hhssnv  21841  shlej2  21940  pjoi0  22296  hodcl  22327  hoadd32  22363  hosubdi  22388  hosubsub2  22392  hoaddsubass  22395  hosubsub4  22398  nmoplb  22487  unop  22495  hmop  22502  nmfnlb  22504  lnopmul  22547  kbass1  22696  kbass2  22697  leopmul2i  22715  leoptr  22717  cvntr  22872  mdslmd4i  22913  mdexchi  22915  atcv1  22960  sumdmdii  22995  xreceu  23105  abfmpel  23219  unitdivcld  23285  logblt  23408  esummulc1  23449  hasheuni  23453  unelsiga  23495  cvmsf1o  23803  cvmscld  23804  vdgrfval  23889  modaddabs  24011  lediv2aALT  24013  mulcan1g  24084  mulcan2g  24085  mulsuble0b  24088  subdivcomb2  24091  gcd32  24104  fununiq  24126  trpredpo  24238  poseq  24253  wfr3g  24255  frr3g  24280  sltres  24318  nocvxmin  24345  dfrdg4  24488  brbtwn2  24533  colinearalg  24538  eleesubd  24540  axcgrrflx  24542  axcgrtr  24543  axsegcon  24555  ax5seglem1  24556  ax5seglem2  24557  ax5seglem4  24560  axbtwnid  24567  axlowdimlem14  24583  axlowdim  24589  axcontlem5  24596  axcontlem7  24598  brcolinear  24682  colinearex  24683  feq123  25068  surjsec2  25120  injsurinj  25149  iscst2  25175  cur1vald  25199  valcurfn1  25204  ubpar  25261  grpodlcan  25376  mvecrtol2  25477  mulinvsca  25480  svli2  25484  truni1  25505  truni3  25507  nelioo5  25511  hmeogrpi  25536  intcont  25543  istopxc  25548  efilcp  25552  cnfilca  25556  cmptdst  25568  limptlimpr2lem1  25574  islimrs4  25582  lvsovso  25626  isaddrv  25646  claddrvr  25648  addcomv  25655  subclrvd  25674  clsmulrv  25683  mulmulvec  25687  hdrmp  25706  idfisf  25841  vtare  25885  vtarsu  25886  tartarmap  25888  fnctartar  25907  cmppar3  25974  nn0prpwlem  26238  clsun  26246  fnemeet1  26315  fnemeet2  26316  fnejoin1  26317  fnejoin2  26318  eltail  26323  cocanfo  26374  f1ocan1fv  26394  incldOLD  26465  metf1o  26469  ismtybnd  26531  ghomco  26573  isdrngo2  26589  inidl  26655  igenmin  26689  mapco2g  26790  mzpcompact2lem  26829  eqrabdioph  26857  lerabdioph  26886  eluzrabdioph  26887  ltrabdioph  26889  nerabdioph  26890  dvdsrabdioph  26891  reglogcl  26975  rmxyadd  27006  rmyabs  27045  congadd  27053  congabseq  27061  rmydioph  27107  uvcresum  27242  lindfmm  27297  lindsmm  27298  symggen  27411  mendrng  27500  mendlmod  27501  dvconstbi  27551  stoweidlem60  27809  wallispilem3  27816  sigarls  27847  frgra3v  28180  3vfriswmgra  28183  bnj545  28927  bnj594  28944  bnj1311  29054  a12study4  29117  lubunNEW  29163  cmtvalN  29401  cvrval  29459  pmapmeet  29962  paddval  29987  paddssat  30003  elpcliN  30082  pclssN  30083  pclunN  30087  paddunN  30116  poldmj1N  30117  tendoplcl2  30967  tendoplcl  30970  dihmeet  31533
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator