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  2619  sbciegft  3034  reuhyp  4578  ordunel  4634  breldmg  4900  funopg  5302  fex2  5417  fvun1  5606  fnreseql  5651  mpt2eq3ia  5929  poxp  6243  smores3  6386  oaord  6561  oacan  6562  oaword  6563  omord  6582  omcan  6583  omwordri  6586  odi  6593  omass  6594  oeord  6602  oecan  6603  oewordri  6606  oeordsuc  6608  nnaord  6633  nnaordr  6634  nndi  6637  nnmass  6638  nnaword  6641  nnmord  6646  nnmwordri  6650  erov  6771  ecopovtrn  6777  ixpf  6854  mapxpen  7043  fimax2g  7119  unbnn  7129  elfiun  7199  suppr  7235  r111  7463  dif1card  7654  xpcdaen  7825  mapcdaen  7826  ackbij1lem16  7877  cff1  7900  cfflb  7901  cfsmolem  7912  fin23lem34  7988  hsmexlem2  8069  axcc3  8080  domtriomlem  8084  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  konigthlem  8206  gchdomtri  8267  tskpr  8408  tskop  8409  tskuni  8421  tskun  8424  gruop  8443  gruun  8444  grudomon  8455  adderpqlem  8594  mulerpqlem  8595  addassnq  8598  mulassnq  8599  distrnq  8601  ltsonq  8609  ltanq  8611  ltmnq  8612  genpass  8649  distrlem1pr  8665  distrlem4pr  8666  ltsopr  8672  adddir  8846  axlttrn  8911  ltletr  8929  letr  8930  mul32  8995  mul31  8996  add32  9042  subsub23  9072  addsubass  9077  subcan2  9088  subsub2  9091  nppcan2  9094  sub32  9097  nnncan  9098  nnncan2  9100  pnpcan2  9103  subdi  9229  subdir  9230  receu  9429  divmul3  9445  divrec  9456  divrec2  9457  divsubdir  9472  divdiv1  9487  redivcl  9495  div2neg  9499  ltmul2  9623  lemul1  9624  lemul2  9625  lemul2a  9627  lediv1  9637  gt0div  9638  ge0div  9639  ltdivmul  9644  ledivmul  9645  ledivmulOLD  9646  ltdivmul2  9647  ledivmul2  9649  ledivmul2OLD  9650  lemuldiv  9651  ltdiv23  9663  lediv23  9664  ledivp1i  9698  ltdivp1i  9699  uzind2  10120  nn0ind  10124  fnn0ind  10127  xrltletr  10504  xrletr  10505  xrre2  10515  xrltmin  10527  xrlemin  10529  xleadd2a  10590  xleadd1  10591  xltadd2  10593  xmulasslem3  10622  xmulass  10623  xltmul2  10629  ixxdisj  10687  iooneg  10772  iccneg  10773  icoshft  10774  icoshftf1o  10775  icodisj  10777  snunioo  10778  fzen  10827  fzrev3  10865  fzoaddel2  10923  modcyc  11015  modcyc2  11016  moddi  11023  modsubdir  11024  expdiv  11168  digit2  11250  ccatass  11452  swrdval  11466  ccatco  11506  shftval2  11586  mulre  11622  absdiv  11796  absdiflt  11817  absdifle  11818  abs3dif  11831  cau3  11855  ello12r  12007  elo12r  12018  geoisum1c  12352  rpnnen2lem4  12512  rpnnen2lem7  12515  dvdsmulc  12572  dvdsmulcr  12574  dvdsmultr1  12579  dvdsmultr2  12580  dvdssub2  12582  oexpneg  12606  divalgb  12619  ndvdsadd  12623  sadass  12678  modgcd  12731  dvdsgcd  12738  dvdsgcdb  12739  gcdass  12740  mulgcd  12741  absmulgcd  12742  rpmulgcd  12750  nn0seqcvgd  12756  algcvga  12765  coprmdvds  12797  coprmdvds2  12798  rpmul  12818  qnumdenbi  12831  coprimeprodsq  12878  pythagtriplem4  12888  pythagtriplem8  12892  pythagtriplem9  12893  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem16  12899  pcpremul  12912  pcgcd  12946  vdwapval  13036  vdwapun  13037  mreiincl  13514  mreincl  13517  mremre  13522  mrcss  13534  catcisolem  13954  pleval2  14115  pospo  14123  clatl  14236  lubss  14241  lubun  14243  clatglbss  14247  ipole  14277  ipolt  14278  pslem  14331  dirtr  14374  gsumws2  14481  frmdmnd  14497  isgrpi  14524  grpsubrcan  14563  grpinvsub  14564  grpsubeq0  14568  grpnpcan  14573  divssub  14693  ghmsub  14707  symggrp  14796  lsmass  14995  efgsrel  15059  cntzcmn  15152  dvrcl  15484  unitdvcl  15485  dvrcan1  15489  subrgmre  15585  abvsubtri  15616  abvtrivd  15621  lmodvsubval2  15696  lss0cl  15720  lssintcl  15737  lssincl  15738  reslmhm2  15826  lspvadd  15865  lspsntrim  15867  islbs3  15924  rrgeq0  16047  cncrng  16411  xrsmcmn  16413  cndrng  16419  cnsrng  16424  xrs1mnd  16425  absabv  16445  unopn  16665  clsss  16807  cldmre  16831  toponmre  16846  opnssneib  16868  restabs  16912  restcls  16927  restntr  16928  hausnei2  17097  cmpsublem  17142  hausmapdom  17242  ptpjcn  17321  upxp  17333  ptrescn  17349  xkopjcn  17366  fbssfi  17548  snfil  17575  ufprim  17620  rnelfm  17664  flimrest  17694  fclsrest  17735  tmdgsum  17794  blpnfctr  17998  mscl  18023  xmscl  18024  xmsge0  18025  xmseq0  18026  ngpds  18141  unitnmn0  18195  xrsxmet  18331  metds0  18370  cncfmptc  18431  cphsqrcl  18636  cfil3i  18711  cfilres  18738  cmmbl  18908  voliunlem2  18924  itg2ub  19104  itgrecl  19168  evlsval2  19420  tdeglem3  19461  r1pid  19561  efgh  19919  eflogeq  19971  cxpadd  20042  lawcos  20130  pythag  20131  asinsinb  20209  acoscosb  20210  atantanb  20236  amgmlem  20300  lgsneg  20574  lgsne0  20588  gxnn0suc  20947  issubgoi  20993  ablomul  21038  imsmetlem  21275  nmoxr  21360  nmoolb  21365  blometi  21397  phpar2  21417  phpar  21418  ipasslem5  21429  hvadd32  21629  hvaddsub12  21633  hvaddsubass  21636  hvsubass  21639  hvsub32  21640  hvsubdistr1  21644  hvsubdistr2  21645  hvmulcan  21667  hvmulcan2  21668  hvsubcan  21669  his5  21681  his2sub  21687  hhssnv  21857  shlej2  21956  pjoi0  22312  hodcl  22343  hoadd32  22379  hosubdi  22404  hosubsub2  22408  hoaddsubass  22411  hosubsub4  22414  nmoplb  22503  unop  22511  hmop  22518  nmfnlb  22520  lnopmul  22563  kbass1  22712  kbass2  22713  leopmul2i  22731  leoptr  22733  cvntr  22888  mdslmd4i  22929  mdexchi  22931  atcv1  22976  sumdmdii  23011  xreceu  23121  abfmpel  23234  unitdivcld  23300  logblt  23423  esummulc1  23464  hasheuni  23468  unelsiga  23510  cvmsf1o  23818  cvmscld  23819  vdgrfval  23904  modaddabs  24026  lediv2aALT  24028  mulcan1g  24099  mulcan2g  24100  mulsuble0b  24103  subdivcomb2  24106  gcd32  24175  fununiq  24197  trpredpo  24309  poseq  24324  wfr3g  24326  frr3g  24351  sltres  24389  nocvxmin  24416  dfrdg4  24560  brbtwn2  24605  colinearalg  24610  eleesubd  24612  axcgrrflx  24614  axcgrtr  24615  axsegcon  24627  ax5seglem1  24628  ax5seglem2  24629  ax5seglem4  24632  axbtwnid  24639  axlowdimlem14  24655  axlowdim  24661  axcontlem5  24668  axcontlem7  24670  brcolinear  24754  colinearex  24755  feq123  25171  surjsec2  25223  injsurinj  25252  iscst2  25278  cur1vald  25302  valcurfn1  25307  ubpar  25364  grpodlcan  25479  mvecrtol2  25580  mulinvsca  25583  svli2  25587  truni1  25608  truni3  25610  nelioo5  25614  hmeogrpi  25639  intcont  25646  istopxc  25651  efilcp  25655  cnfilca  25659  cmptdst  25671  limptlimpr2lem1  25677  islimrs4  25685  lvsovso  25729  isaddrv  25749  claddrvr  25751  addcomv  25758  subclrvd  25777  clsmulrv  25786  mulmulvec  25790  hdrmp  25809  idfisf  25944  vtare  25988  vtarsu  25989  tartarmap  25991  fnctartar  26010  cmppar3  26077  nn0prpwlem  26341  clsun  26349  fnemeet1  26418  fnemeet2  26419  fnejoin1  26420  fnejoin2  26421  eltail  26426  cocanfo  26477  f1ocan1fv  26497  incldOLD  26568  metf1o  26572  ismtybnd  26634  ghomco  26676  isdrngo2  26692  inidl  26758  igenmin  26792  mapco2g  26893  mzpcompact2lem  26932  eqrabdioph  26960  lerabdioph  26989  eluzrabdioph  26990  ltrabdioph  26992  nerabdioph  26993  dvdsrabdioph  26994  reglogcl  27078  rmxyadd  27109  rmyabs  27148  congadd  27156  congabseq  27164  rmydioph  27210  uvcresum  27345  lindfmm  27400  lindsmm  27401  symggen  27514  mendrng  27603  mendlmod  27604  dvconstbi  27654  stoweidlem60  27912  wallispilem3  27919  sigarls  27950  nb3graprlem2  28288  cusgra3v  28299  usgrnloop  28351  redwlk  28364  cyclispthon  28378  usgrcyclnl1  28386  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3lem5  28394  constr3trllem2  28397  constr3pthlem2  28402  4cycl4v4e  28412  4cycl4dv4e  28414  frgra3v  28426  3vfriswmgra  28429  bnj545  29243  bnj594  29260  bnj1311  29370  a12study4  29739  lubunNEW  29785  cmtvalN  30023  cvrval  30081  pmapmeet  30584  paddval  30609  paddssat  30625  elpcliN  30704  pclssN  30705  pclunN  30709  paddunN  30738  poldmj1N  30739  tendoplcl2  31589  tendoplcl  31592  dihmeet  32155
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