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

Theorem 3ad2ant3 1017
Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
Hypothesis
Ref Expression
3ad2ant.1  |-  ( ph  ->  ch )
Assertion
Ref Expression
3ad2ant3  |-  ( ( ps  /\  th  /\  ph )  ->  ch )

Proof of Theorem 3ad2ant3
StepHypRef Expression
1 3ad2ant.1 . . 3  |-  ( ph  ->  ch )
21adantl 464 . 2  |-  ( ( th  /\  ph )  ->  ch )
323adant1 1012 1  |-  ( ( ps  /\  th  /\  ph )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simp3l  1022  simp3r  1023  simp31  1030  simp32  1031  simp33  1032  simp3ll  1065  simp3lr  1066  simp3rl  1067  simp3rr  1068  simp3l1  1099  simp3l2  1100  simp3l3  1101  simp3r1  1102  simp3r2  1103  simp3r3  1104  simp31l  1117  simp31r  1118  simp32l  1119  simp32r  1120  simp33l  1121  simp33r  1122  simp311  1141  simp312  1142  simp313  1143  simp321  1144  simp322  1145  simp323  1146  simp331  1147  simp332  1148  simp333  1149  3anim123i  1179  3jaao  1294  ceqsalt  3057  ceqsralt  3058  vtoclgft  3082  euelss  3710  tpssi  4110  prnebg  4126  otthg  4645  poltletr  5312  funprg  5545  funtpg  5546  fntpg  5551  ftpg  5983  fsnunf  6011  fsnunfv  6013  fvpr1g  6018  fvpr2g  6019  fnsuppresOLD  6033  weniso  6151  ovmpt3rab1  6433  epne3  6515  limsuc  6583  oteqimp  6718  el2xptp0  6743  funsssuppss  6844  smoel  6949  smoord  6954  omwordi  7138  oneo  7148  oeord  7155  oewordi  7158  nnmwordi  7202  nnneo  7218  uniinqs  7309  undifixp  7424  enfixsn  7545  domss2  7595  domssex2  7596  unxpdomlem3  7642  dif1en  7668  mapfien2  7783  dffi2  7798  unwdomg  7925  ixpiunwdom  7932  en3lplem1  7945  oemapvali  8016  fodomfi2  8354  infcdaabs  8499  infunabs  8500  infdif  8502  ackbij1lem9  8521  ackbij1lem16  8528  coflim  8554  cfsmolem  8563  isfin2-2  8612  fin1a2lem9  8701  hsmexlem2  8720  axcc2lem  8729  axcc3  8731  domtriomlem  8735  axdc3lem4  8746  axcclem  8750  zornn0g  8798  axacndlem4  8899  axacndlem5  8900  axacnd  8901  gchdomtri  8918  fpwwe  8935  tskssel  9046  tskint  9074  tskurn  9078  gruurn  9087  gruixp  9098  grudomon  9106  gruina  9107  adderpqlem  9243  mulerpqlem  9244  addassnq  9247  mulassnq  9248  distrnq  9250  ltsonq  9258  ltanq  9260  ltmnq  9261  reclem3pr  9338  dedekind  9655  addid2  9674  addcan2  9676  divdir  10147  divcan5  10163  ltdiv1  10323  infmrcl  10438  infmrlb  10440  lt2halves  10690  zdivmul  10852  xaddass  11362  xleadd1  11368  xltadd1  11369  xmulasslem3  11399  xmulass  11400  xlemul1  11403  xlemul2  11404  xltmul1  11405  xadddir  11409  elioo5  11503  iccsupr  11538  iccneg  11562  icoshft  11563  icoshftf1o  11564  iccsplit  11574  fzen  11624  elfz1b  11670  fzrevral  11685  fzshftral  11688  elfz0ubfz0  11700  elfz0fzfz0  11701  fz0fzelfz0  11702  fz0fzdiffz0  11705  elfzo  11724  elfzonlteqm1  11790  ltdifltdiv  11866  modabs  11930  modcyc  11932  modaddmulmod  11956  moddi  11957  modsubdir  11958  expdiv  12119  leexp2a  12124  bcval3  12286  hashnnn0genn0  12318  hashgadd  12348  hashunx  12357  hashfun  12399  hashtpg  12427  brfi1indlem  12435  ccatval1  12504  ccatval2  12505  ccatval3  12506  ccatsymb  12509  ccatass  12514  ccats1val2  12540  swrdval2  12556  swrd0len0  12572  swrd0fv  12575  swrdeq  12580  swrdspsleq  12585  2swrdeqwrdeq  12589  swrdswrdlem  12595  swrdswrd  12596  swrd0swrd  12597  ccats1swrdeq  12605  ccats1swrdeqrex  12615  swrdccatin12lem2  12625  swrdccat3b  12632  swrdccatid  12633  splval  12638  repswswrd  12667  cshwidxmod  12685  cshwidx0mod  12686  cshwleneq  12696  scshwfzeqfzo  12705  ccatco  12712  cshco  12713  swrdco  12714  f1oun2prg  12776  swrds2  12794  trclfvss  12844  elicc4abs  13154  mulcn2  13420  fsumsplitsnun  13572  modfsummods  13609  prodfrec  13706  ntrivcvgfvn0  13710  demoivreALT  13938  rpnnen2lem4  13953  dvdsval2  13991  dvdsexp  14044  mulgcd  14186  mulgcdr  14188  gcddiv  14189  rpmulgcd  14195  rplpwr  14196  prmexpb  14260  rpexp  14263  modprm0  14332  modprmn0modprm0  14334  coprimeprodsq  14335  pythagtriplem1  14342  pythagtriplem3  14344  pythagtriplem10  14346  pythagtriplem6  14347  pythagtriplem11  14351  pythagtriplem12  14352  pythagtriplem13  14353  pythagtriplem15  14355  pythagtriplem17  14357  pythagtriplem19  14359  pcdvdsb  14394  pcfaclem  14419  vdwapun  14494  ramval  14528  0ram2  14541  0ramcl  14543  imasaddvallem  14936  imasvscaval  14945  mreiincl  15003  mremre  15011  mrieqv2d  15046  cofurid  15297  initoeu2lem0  15409  initoeu2lem2  15411  funcestrcsetclem6  15531  funcestrcsetclem9  15534  funcsetcestrclem6  15546  funcsetcestrclem9  15549  xpcpropd  15594  clatleglb  15873  ress0g  16066  gsumccat  16126  gsumccatsn  16128  sgrp2nmndlem3  16160  sgrp2nmndlem5  16164  mulgdirlem  16283  mulgp1  16285  eqglact  16369  fvcosymgeq  16571  gsmsymgreqlem2  16573  pmtrprfv3  16596  pmtr3ncomlem1  16615  mndodcongi  16684  oddvdsnn0  16685  odngen  16714  gexnnod  16725  lsmlub  16800  lsmass  16805  efgsval2  16868  efgsrel  16869  ghmplusg  16969  odadd1  16971  odadd2  16972  srg1zr  17293  dvrcan1  17453  dvrcan3  17454  irredrmul  17469  srngadd  17619  srngmul  17620  lmhmvsca  17804  reslmhm2  17812  pwssplit3  17820  lbspss  17841  lsmsp  17845  lspsneu  17882  lidldvgen  18016  assa2ass  18084  evlsval  18301  evlsval2  18302  psropprmul  18392  coe1add  18418  coe1addfv  18419  coe1subfv  18420  coe1tm  18427  coe1sclmul  18436  coe1sclmul2  18438  coe1fzgsumdlem  18456  lply1binom  18461  evl1gsumdlem  18505  zrhpsgninv  18712  zrhpsgnevpm  18718  zrhpsgnodpm  18719  psgndiflemB  18727  cssmre  18815  frlmup4  18921  islindf2  18934  lindsind2  18939  f1lindf  18942  lindsss  18944  f1linds  18945  lindsmm  18948  lbslcic  18961  mndvcl  18978  mndvass  18979  mhmvlin  18984  matecl  19012  matvscacell  19023  mamulid  19028  mamurid  19029  mattposm  19046  madetsumid  19048  matepmcl  19049  matepm2cl  19050  mat1dimbas  19059  mavmulsolcl  19138  mulmarep1el  19159  mulmarep1gsum1  19160  mulmarep1gsum2  19161  1marepvsma1  19170  m1detdiag  19184  mdetdiaglem  19185  mdetdiag  19186  mdetunilem7  19205  mdetunilem9  19207  mdetmul  19210  gsummatr01lem3  19244  gsummatr01lem4  19245  gsummatr01  19246  smadiadetglem2  19259  matinv  19264  slesolinv  19267  cramerimplem1  19270  cramerimp  19273  cramerlem1  19274  pmatcoe1fsupp  19287  mat2pmatbas  19312  decpmatmullem  19357  pmatcollpw3lem  19369  chpscmat  19428  iuncld  19631  clsss  19640  ntrcls0  19663  iscldtop  19682  neiss  19696  neips  19700  restcldi  19760  cnpnei  19851  cnconst2  19870  cnpresti  19875  sslm  19886  cnt0  19933  cnt1  19937  cnhaus  19941  cncmp  19978  cmpcld  19988  cnconn  20008  concompss  20019  ssref  20098  elptr  20159  upxp  20209  qtoptop2  20285  ordthmeolem  20387  opnfbas  20428  isfil2  20442  fbasweak  20451  snfbas  20452  fgss  20459  fgcl  20464  fbasrn  20470  trnei  20478  cfinfil  20479  csdfil  20480  supfil  20481  filufint  20506  fin1aufil  20518  fmval  20529  fmf  20531  elfm  20533  elfm3  20536  imaelfm  20537  rnelfmlem  20538  rnelfm  20539  flimclslem  20570  flfneii  20578  cnpfcfi  20626  alexsubALT  20636  ptcmplem3  20639  ustref  20806  ustelimasn  20810  utop3cls  20839  ressusp  20853  cfiluexsm  20878  prdsxmetlem  20956  txmetcn  21136  nmmtri  21226  nmrtri  21228  unitnmn0  21262  nminvr  21263  nmotri  21331  nghmplusg  21332  isclmi  21662  fmcfil  21796  srabn  21885  rrxmvallem  21916  itgconst  22310  dvn2bss  22418  deg1mul3  22601  deg1mul3le  22602  deg1tmle  22603  q1peqb  22640  r1pcl  22643  r1pdeglt  22644  r1pid  22645  dvdsq1p  22646  dvdsr1p  22647  ptolemy  22974  sincosq1eq  22990  logeq0im1  23050  logmul2  23088  logdiv2  23089  cxplt2  23166  logbchbase  23229  relogbreexp  23233  relogbexp  23238  pythag  23267  bcmono  23669  efexple  23673  lgsdirnn0  23731  selberglem3  23849  brbtwn2  24329  axcgrid  24340  ax5seglem1  24352  ax5seglem2  24353  ax5seg  24362  axpasch  24365  axlowdimlem16  24381  axcontlem7  24394  nbgraf1olem1  24562  nbusgrafi  24569  nb3graprlem1  24572  nb3graprlem2  24573  cusgra2v  24583  cusgra3v  24585  wlkcomp  24646  wlkelwrd  24651  2trllemH  24675  2trllemE  24676  constr1trl  24711  constr2spthlem1  24717  2pthlem2  24719  2wlklem1  24720  2pthon  24725  usgra2adedgwlkonALT  24737  constr3lem4  24768  constr3trllem2  24772  constr3trllem5  24775  constr3pthlem2  24777  wlkiswwlk2  24818  2wlkeq  24828  usg2wlkeq  24829  usg2wlkeq2  24830  wwlknred  24844  wwlknext  24845  wwlknredwwlkn  24847  wwlknfi  24859  wlknfi  24860  wlknwwlknvbij  24861  wwlkextproplem3  24864  clwlkcomp  24884  clwwlkgt0  24892  clwwlknprop  24893  clwwlkn0  24895  clwwlkel  24914  clwwlkf  24915  clwwlkf1  24917  clwwlkfo  24918  clwwlkvbij  24922  clwwlkext2edg  24923  clwwisshclwwlem1  24926  clwwisshclww  24928  clwwnisshclwwn  24930  erclwwlkeqlen  24933  erclwwlkref  24934  eleclclwwlknlem2  24939  erclwwlkneqlen  24945  erclwwlknref  24946  erclwwlknsym  24947  erclwwlkntr  24948  hashecclwwlkn1  24955  usghashecclwwlk  24956  hashclwwlkn  24957  clwwlkndivn  24958  clwlkfclwwlk  24965  clwlkfoclwwlk  24966  clwlkf1clwwlklem  24970  clwlkf1clwwlk  24971  el2wlkonot  24990  el2spthonot  24991  el2spthonot0  24992  el2wlkonotot0  24993  vdgrfival  25018  vdgrf  25019  vdgrfif  25020  vdusgra0nedg  25029  hashnbgravd  25033  nbhashnn0  25035  isrgra  25047  rusgranumwwlkl1  25067  rusgra0edg  25076  rusgranumwlks  25077  3vfriswmgralem  25125  3vfriswmgra  25126  usgn0fidegnn0  25150  2spotdisj  25182  usg2spot2nb  25186  extwwlkfablem1  25195  clwwlkextfrlem1  25197  extwwlkfablem2  25199  numclwwlkun  25200  numclwwlkovf2ex  25207  extwwlkfab  25211  numclwlk1lem2foa  25212  numclwlk1lem2f1  25215  numclwlk1lem2fo  25216  numclwwlk1  25219  numclwwlk2lem1  25223  numclwlk2lem2f  25224  numclwlk2lem2f1o  25226  numclwwlk2  25228  numclwwlk3  25230  numclwwlk4  25231  numclwwlk6  25234  numclwwlk7  25235  numclwwlk8  25236  frgrareg  25238  frgraregord013  25239  gxpval  25378  gxnval  25379  gxnn0neg  25382  gxnn0suc  25383  gxneg  25385  gxsuc  25391  gxnn0add  25393  gxadd  25394  gxsub  25395  gxnn0mul  25396  gxmul  25397  gxmodid  25398  gxdi  25415  zerdivemp1  25553  rngoridfz  25554  vcid  25561  vcdi  25562  vcdir  25563  vcass  25564  imsmetlem  25713  0oval  25820  ajval  25894  shlub  26449  hmopco  27058  adjlnop  27121  mdslmd4i  27368  fcoinvbr  27594  fresf1o  27611  divnumden2  27762  ressnm  27792  ress1r  27933  pstmfval  28029  pl1cn  28091  ind1  28167  ind0  28168  sigaclcuni  28267  sigagenss2  28299  measun  28338  measvuni  28341  dya2iocnrect  28408  omsmeas  28450  ballotlemieq  28638  ballotlemrv1  28642  sgn3da  28663  lgamgulmlem1  28760  erdszelem2  28825  cnpcon  28864  cvmscld  28907  mrsubcv  29059  mrsubvr  29060  ghomf1olem  29223  iprodefisumlem  29289  binomrisefac  29330  dvdspw  29341  dfon2lem3  29382  dfon2lem7  29386  predeq123  29410  predpo  29429  frrlem4  29555  nofulllem3  29629  btwndiff  29830  brcolinear2  29861  btwnconn1  29904  nnssi3  30074  nndivsub  30075  ftc1anclem4  30259  areacirclem2  30274  areacirclem5  30277  areacirc  30278  nn0prpwlem  30306  hmeoclda  30317  hmeocldb  30318  ivthALT  30319  fnemeet1  30350  fnejoin1  30352  upixp  30386  filbcmb  30397  cnresima  30426  smprngopr  30615  igenval2  30629  ismrcd1  30796  istopclsd  30798  ismrc  30799  mapfzcons  30814  eldioph2  30860  diophrex  30874  diophren  30912  pellexlem1  30930  pellexlem5  30934  pellqrexplicit  30978  reglogmul  30994  reglogexp  30995  rmxycomplete  31018  congmul  31070  congabseq  31077  acongsym  31079  acongneg2  31080  fzneg  31085  acongeq  31086  jm2.19  31101  jm2.22  31103  jm2.23  31104  jm2.20nn  31105  rmydioph  31122  rmxdiophlem  31123  jm3.1  31128  pwssplit4  31201  mapfien2OLD  31208  hbtlem2  31241  idomrootle  31320  dvconstbi  31407  expgrowth  31408  fmul01lt1lem1  31744  climsuselem1  31779  climsuse  31780  limcperiod  31800  lptre2pt  31812  cncfshift  31842  cncfperiod  31847  icccncfext  31856  dvnmptconst  31904  dvnprodlem1  31909  dvnprodlem2  31910  iblspltprt  31938  itgspltprt  31944  stoweidlem3  31951  stoweidlem16  31964  stoweidlem17  31965  stoweidlem26  31974  stoweidlem34  31982  stoweidlem57  32005  fourierdlem41  32096  fourierdlem42  32097  fourierdlem52  32107  fourierdlem54  32109  fourierdlem74  32129  fourierdlem75  32130  fourierdlem80  32135  fourierdlem94  32149  fourierdlem102  32157  fourierdlem114  32169  etransclem18  32201  etransclem29  32212  etransclem46  32229  oexpnegnz  32520  pfxnd  32570  pfxlen0  32571  pfxfv  32574  pfxeq  32579  pfxsuffeqwrdeq  32581  pfxpfx  32590  ccats1pfxeq  32596  ccats1pfxeqrex  32597  pfxccatin12lem2  32599  pfxccatpfx1  32602  pfxccatid  32605  repswpfx  32611  elpwdifsn  32617  2leaddle2  32641  ssfz12  32651  fsumsplitsndif  32664  fsummmodsndifre  32665  fsummmodsnunz  32666  usgra2pth  32672  usgvincvad  32722  usgvincvadALT  32725  rngdir  32888  c0snmhm  32921  rngccatidALTV  32997  funcringcsetcALTV2lem6  33049  funcringcsetcALTV2lem9  33052  ringccatidALTV  33060  funcringcsetclem6ALTV  33072  ofaddmndmap  33133  mapprop  33135  nn0sumltlt  33139  gsumpr  33150  domnmsuppn0  33162  scmsuppss  33165  mndpsuppfi  33168  gsumlsscl  33176  ply1ass23l  33182  ply1mulgsumlem1  33186  lincfsuppcl  33214  linccl  33215  lincvalsng  33217  lincvalpr  33219  lincdifsn  33225  ellcoellss  33236  lincext1  33255  lincext2  33256  lincext3  33257  lindslinindimp2lem2  33260  ldepspr  33274  lincresunit3lem1  33280  lincresunit3lem2  33281  islindeps2  33284  logcxp0  33356  elbigo2r  33374  elbigolo1  33378  fllog2  33389  nnolog2flm1  33411  digvalnn0  33420  nn0digval  33421  dignn0fr  33422  dignn0ldlem  33423  dignnld  33424  digexp  33428  dignn0flhalflem1  33436  dignn0flhalflem2  33437  dignn0ehalf  33438  dignn0flhalf  33439  chordthmALT  34080  bnj837  34166  bnj517  34290  bnj553  34303  bnj594  34317  bnj967  34350  bnj1097  34384  bnj1110  34385  bnj1118  34387  bnj1128  34393  bnj1125  34395  bnj1145  34396  bnj1136  34400  bnj1173  34405  bnj1189  34412  bnj1204  34415  bnj1279  34421  bnj1321  34430  bnj1413  34438  bj-ceqsalt1  34797  lsmsat  35146  lsmsatcv  35148  lsatcvatlem  35187  islshpcv  35191  l1cvpat  35192  lfli  35199  lshpset2N  35257  cvrnbtwn  35409  meetat2  35435  atcmp  35449  atcvreq0  35452  atlatmstc  35457  cvlcvr1  35477  cvlcvrp  35478  cvlatcvr2  35480  cvr2N  35548  cvratlem  35558  2atjm  35582  athgt  35593  2lplnmN  35696  2llnmj  35697  2lplnmj  35759  dalemswapyzps  35827  dalem23  35833  dalem24  35834  dalem25  35835  dalem27  35836  dalem28  35837  dalem38  35847  dalem39  35848  dalem44  35853  dalem45  35854  dalem51  35860  dalem52  35861  dalem56  35865  pmapglbx  35906  pmapjat1  35990  pmapjat2  35991  paddatclN  36086  osumcllem4N  36096  osumcllem7N  36099  ltrncoval  36282  cdleme0aa  36348  cdleme0b  36350  cdleme8  36388  cdlemesner  36434  cdleme22eALTN  36484  cdleme26eALTN  36500  cdleme35h  36595  cdleme50trn2  36690  cdleme  36699  tgrpov  36887  tendotp  36900  tendoidcl  36908  tendo0co2  36927  cdlemkvcl  36981  dvhopvadd  37233  dvhopellsm  37257  dihmeetlem1N  37430  dihmeetlem9N  37455  dihatexv  37478  lcfl7lem  37639  mapdrvallem2  37785  mapdh9a  37930  hdmapevec  37978  pwinfi2  38176  relexpaddss  38223  trclimalb2  38257  brtrclfv2  38258
  Copyright terms: Public domain W3C validator