Theorem 3ad2ant3 1084

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

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantl 482	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 1079	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simp3l  1089  simp3r  1090  simp31  1097  simp32  1098  simp33  1099  simp3ll  1132  simp3lr  1133  simp3rl  1134  simp3rr  1135  simp3l1  1166  simp3l2  1167  simp3l3  1168  simp3r1  1169  simp3r2  1170  simp3r3  1171  simp31l  1184  simp31r  1185  simp32l  1186  simp32r  1187  simp33l  1188  simp33r  1189  simp311  1208  simp312  1209  simp313  1210  simp321  1211  simp322  1212  simp323  1213  simp331  1214  simp332  1215  simp333  1216  3anim123i  1247  3jaao  1396  ceqsalt  3228  ceqsralt  3229  vtoclgftOLD  3255  disjtpsn  4251  disjtp2  4252  elpwdifsn  4319  ssprsseq  4357  tpssi  4369  prnebg  4389  poltletr  5528  predeq123  5681  predpo  5698  funprgOLD  5941  funtpgOLD  5943  fntpg  5948  funcnvpr  5950  funcnvtp  5951  ftpg  6423  fsnunf  6451  fsnunfv  6453  fvpr1g  6458  fvpr2g  6459  fpropnf1  6524  weniso  6604  ovmpt3rab1  6891  epne3  6980  limsuc  7049  oteqimp  7187  el2xptp0  7212  funsssuppss  7321  smoel  7457  smoord  7462  omwordi  7651  oneo  7661  oeord  7668  oewordi  7671  nnmwordi  7715  nnneo  7731  uniinqs  7827  undifixp  7944  enfixsn  8069  domss2  8119  domssex2  8120  unxpdomlem3  8166  dif1en  8193  rneqdmfinf1o  8242  mapfien2  8314  dffi2  8329  unwdomg  8489  ixpiunwdom  8496  en3lplem1  8511  oemapvali  8581  fodomfi2  8883  infcdaabs  9028  infunabs  9029  infdif  9031  ackbij1lem9  9050  ackbij1lem16  9057  coflim  9083  cfsmolem  9092  isfin2-2  9141  fin1a2lem9  9230  hsmexlem2  9249  axcc2lem  9258  axcc3  9260  domtriomlem  9264  axdc3lem4  9275  axcclem  9279  zornn0g  9327  axacndlem4  9432  axacndlem5  9433  axacnd  9434  gchdomtri  9451  fpwwe  9468  tskssel  9579  tskint  9607  tskurn  9611  gruurn  9620  gruixp  9631  grudomon  9639  gruina  9640  adderpqlem  9776  mulerpqlem  9777  addassnq  9780  mulassnq  9781  distrnq  9783  ltsonq  9791  ltanq  9793  ltmnq  9794  reclem3pr  9871  dedekind  10200  addid2  10219  addcan2  10221  divdir  10710  divcan5  10727  ltdiv1  10887  infrelb  11008  lt2halves  11267  zdivmul  11449  ledivge1le  11901  addlelt  11942  xaddass  12079  xleadd1  12085  xltadd1  12086  xmulasslem3  12116  xmulass  12117  xlemul1  12120  xlemul2  12121  xltmul1  12122  xadddir  12126  elioo5  12231  iccsupr  12266  iccneg  12293  icoshft  12294  icoshftf1o  12295  iccsplit  12305  zltaddlt1le  12324  fzen  12358  ssfzunsn  12387  elfz1b  12409  fzrevral  12425  fzshftral  12428  elfz0ubfz0  12443  elfz0fzfz0  12444  fz0fzelfz0  12445  fz0fzdiffz0  12448  elfzo  12472  elfzonlteqm1  12543  ltdifltdiv  12635  modabs  12703  modcyc  12705  modaddmulmod  12737  moddi  12738  modsubdir  12739  expdiv  12911  leexp2a  12916  bcval3  13093  hashnnn0genn0  13131  hashgadd  13166  hashunx  13175  hashfun  13224  hashres  13225  hash2prd  13257  hashtpg  13267  fun2dmnop0  13276  brfi1indlem  13278  ccatval1  13361  ccatval2  13362  ccatval3  13363  ccatsymb  13366  ccatass  13371  ccats1val2  13404  swrdval2  13420  swrd0len0  13436  swrd0fv  13439  swrdeq  13444  swrdspsleq  13449  2swrdeqwrdeq  13453  swrdswrdlem  13459  swrdswrd  13460  swrd0swrd  13461  ccats1swrdeq  13469  ccats1swrdeqrex  13478  swrdccatin12lem2  13489  swrdccat3b  13496  swrdccatid  13497  splval  13502  repswswrd  13531  cshwidxmod  13549  cshwidx0mod  13551  cshf1  13556  cshwleneq  13563  scshwfzeqfzo  13572  cshimadifsn  13575  cshimadifsn0  13576  ccatco  13581  cshco  13582  swrdco  13583  f1oun2prg  13662  swrds2  13685  eqwrds3  13704  trclfvss  13747  elicc4abs  14059  mulcn2  14326  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  modfsummods  14525  prodfrec  14627  ntrivcvgfvn0  14631  binomrisefac  14773  demoivreALT  14931  rpnnen2lem4  14946  dvdsval2  14986  modmulconst  15013  dvdsexp  15049  oddge22np1  15073  modremain  15132  mulgcd  15265  mulgcdr  15267  gcddiv  15268  rpmulgcd  15275  rplpwr  15276  lcmfn0val  15336  lcmftp  15349  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  coprmdvds  15366  cncongr1  15381  dvdsnprmd  15403  prmexpb  15430  rpexp  15432  cncongrprm  15437  modprm0  15510  modprmn0modprm0  15512  coprimeprodsq  15513  pythagtriplem1  15521  pythagtriplem3  15523  pythagtriplem10  15525  pythagtriplem6  15526  pythagtriplem11  15530  pythagtriplem12  15531  pythagtriplem13  15532  pythagtriplem15  15534  pythagtriplem17  15536  pythagtriplem19  15538  pcdvdsb  15573  dvdsprmpweqle  15590  pcfaclem  15602  vdwapun  15678  ramval  15712  0ram2  15725  0ramcl  15727  fvprmselgcd1  15749  prmgaplem6  15760  setsstructOLD  15899  imasaddvallem  16189  imasvscaval  16198  mreiincl  16256  mremre  16264  mrieqv2d  16299  cofurid  16551  initoeu2lem0  16663  initoeu2lem2  16665  funcestrcsetclem6  16785  funcestrcsetclem9  16788  funcsetcestrclem6  16800  funcsetcestrclem9  16803  xpcpropd  16848  clatleglb  17126  ress0g  17319  gsumccat  17378  gsumccatsn  17380  sgrp2nmndlem3  17412  sgrp2nmndlem5  17416  dfgrp3lem  17513  mulgdirlem  17572  mulgp1  17574  mulgmodid  17581  eqglact  17645  fvcosymgeq  17849  gsmsymgreqlem2  17851  pmtrprfv3  17874  pmtr3ncomlem1  17893  mndodcongi  17962  oddvdsnn0  17963  odngen  17992  gexnnod  18003  lsmlub  18078  lsmass  18083  efgsval2  18146  efgsrel  18147  ghmplusg  18249  odadd1  18251  odadd2  18252  srg1zr  18529  dvrcan1  18691  dvrcan3  18692  irredrmul  18707  srngadd  18857  srngmul  18858  rmodislmodlem  18930  rmodislmod  18931  lmhmvsca  19045  reslmhm2  19053  pwssplit3  19061  lbspss  19082  lsmsp  19086  lspsneu  19123  lidldvgen  19255  assa2ass  19322  evlsval  19519  evlsval2  19520  psropprmul  19608  coe1add  19634  coe1addfv  19635  coe1subfv  19636  coe1tm  19643  coe1sclmul  19652  coe1sclmul2  19654  coe1fzgsumdlem  19671  lply1binom  19676  evl1gsumdlem  19720  zrhpsgninv  19931  zrhpsgnevpm  19937  zrhpsgnodpm  19938  psgndiflemB  19946  cssmre  20037  frlmup4  20140  islindf2  20153  lindsind2  20158  f1lindf  20161  lindsss  20163  f1linds  20164  lindsmm  20167  lbslcic  20180  mndvcl  20197  mndvass  20198  mhmvlin  20203  matecl  20231  matvscacell  20242  mamulid  20247  mamurid  20248  mattposm  20265  madetsumid  20267  matepmcl  20268  matepm2cl  20269  mat1dimbas  20278  mavmulsolcl  20357  mulmarep1el  20378  mulmarep1gsum1  20379  mulmarep1gsum2  20380  1marepvsma1  20389  m1detdiag  20403  mdetdiaglem  20404  mdetdiag  20405  mdetunilem7  20424  mdetunilem9  20426  mdetmul  20429  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  smadiadetglem2  20478  matinv  20483  slesolinv  20486  cramerimplem1  20489  cramerimp  20492  cramerlem1  20493  pmatcoe1fsupp  20506  mat2pmatbas  20531  decpmatmullem  20576  pmatcollpw3lem  20588  chpscmat  20647  iuncld  20849  clsss  20858  ntrcls0  20880  iscldtop  20899  neiss  20913  neips  20917  restcldi  20977  cnpnei  21068  cnconst2  21087  cnpresti  21092  sslm  21103  cnt0  21150  cnt1  21154  cnhaus  21158  cncmp  21195  cmpcld  21205  cnconn  21225  conncompss  21236  ssref  21315  elptr  21376  upxp  21426  qtoptop2  21502  ordthmeolem  21604  opnfbas  21646  isfil2  21660  fbasweak  21669  snfbas  21670  fgss  21677  fgcl  21682  fbasrn  21688  trnei  21696  cfinfil  21697  csdfil  21698  supfil  21699  filufint  21724  fin1aufil  21736  fmval  21747  fmf  21749  elfm  21751  elfm3  21754  imaelfm  21755  rnelfmlem  21756  rnelfm  21757  flimclslem  21788  flfneii  21796  cnpfcfi  21844  alexsubALT  21855  ptcmplem3  21858  ustref  22022  ustelimasn  22026  utop3cls  22055  ressusp  22069  cfiluexsm  22094  prdsxmetlem  22173  txmetcn  22353  nmmtri  22426  nmrtri  22428  unitnmn0  22472  nminvr  22473  nmotri  22543  nghmplusg  22544  isclmi  22877  isclmp  22897  ncvsi  22951  fmcfil  23070  srabn  23156  rrxmvallem  23187  itgconst  23585  dvn2bss  23693  deg1mul3  23875  deg1mul3le  23876  deg1tmle  23877  q1peqb  23914  r1pcl  23917  r1pdeglt  23918  r1pid  23919  dvdsq1p  23920  dvdsr1p  23921  ptolemy  24248  sincosq1eq  24264  logeq0im1  24324  logmul2  24362  logdiv2  24363  cxplt2  24444  logbchbase  24509  relogbreexp  24513  relogbexp  24518  pythag  24547  lgamgulmlem1  24755  bcmono  25002  efexple  25006  lgsdirnn0  25069  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  2lgslem1a1  25114  2lgsoddprmlem1  25133  2lgsoddprmlem2  25134  selberglem3  25236  brbtwn2  25785  axcgrid  25796  ax5seglem1  25808  ax5seglem2  25809  ax5seg  25818  axpasch  25821  axlowdimlem16  25837  axcontlem7  25850  structiedg0val  25911  lpvtx  25963  incistruhgr  25974  upgredg2vtx  26036  upgredgpr  26037  edglnl  26038  ausgrumgri  26062  ausgrusgri  26063  usgredg2vtxeuALT  26114  ushgredgedg  26121  ushgredgedgloop  26123  uspgr1v1eop  26141  usgr1v0edg  26149  uhgrissubgr  26167  egrsubgr  26169  0uhgrsubgr  26171  nbupgrres  26266  nb3grprlem1  26282  cplgr3v  26331  umgr2v2enb1  26422  finsumvtxdgeven  26448  vtxdgoddnumeven  26449  rusgrnumwrdl2  26482  rusgr1vtx  26484  isewlk  26498  ewlkinedg  26500  upgrewlkle2  26502  wlkvtxeledg  26519  wlkeq  26529  wlkl1loop  26534  wlk1walk  26535  uspgr2wlkeq  26542  uspgr2wlkeq2  26543  wlksoneq1eq2  26560  wlkonl1iedg  26561  wlkon2n0  26562  wlkres  26567  wlkp1lem8  26577  lfgriswlk  26585  lfgrwlknloop  26586  spthonpthon  26647  spthonepeq  26648  uhgrwkspth  26651  usgr2wlkspth  26655  usgr2pth  26660  wwlknp  26734  0enwwlksnge1  26749  wwlksnred  26787  wwlksnredwwlkn  26790  wwlksnextsur  26795  wlksnwwlknvbij  26803  umgr2adedgwlkonALT  26843  umgr2wlkon  26846  umgrwwlks2on  26850  elwspths2spth  26862  rusgr0edg  26868  rusgrnumwwlks  26869  clwwlkinwwlk  26905  clwwlksf  26915  clwwlksvbij  26922  clwwlksext2edg  26923  clwwisshclwwslemlem  26926  clwlksfclwwlk  26962  clwlksf1clwwlklem2  26966  clwlksf1clwwlklem  26968  clwwlksnun  26974  1ewlk  26976  1pthon2v  27013  3wlkdlem9  27028  uhgr3cyclex  27042  umgr3cyclex  27043  upgr4cycl4dv4e  27045  upgreupthseg  27069  eupth2lem3lem6  27093  eulercrct  27102  nfrgr2v  27136  frgr3vlem1  27137  3vfriswmgr  27142  extwwlkfablem1  27207  numclwwlkovf2exlem2  27212  numclwwlkovf2ex  27219  numclwlk1lem2foalem  27222  extwwlkfab  27223  numclwlk1lem2foa  27224  numclwlk1lem2f1  27227  numclwlk1lem2fo  27228  numclwwlk1  27231  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  numclwwlk2  27240  numclwwlk3OLD  27242  numclwwlk3  27243  numclwwlk5lem  27245  numclwwlk6  27248  frgrreggt1  27251  frgrreg  27252  frgrregord013  27253  vcidOLD  27419  vcdi  27420  vcdir  27421  vcass  27422  imsmetlem  27545  0oval  27643  ajval  27717  shlub  28273  hmopco  28882  adjlnop  28945  mdslmd4i  29192  fcoinvbr  29419  fresf1o  29433  divnumden2  29564  ressnm  29651  ress1r  29789  smatfval  29861  pstmfval  29939  pl1cn  30001  ind1  30079  ind0  30080  sigaclcuni  30181  sigagenss2  30213  measun  30274  measvuni  30277  dya2iocnrect  30343  omsmeas  30385  ballotlemieq  30578  ballotlemrv1  30582  sgn3da  30603  bnj837  30831  bnj517  30955  bnj553  30968  bnj594  30982  bnj967  31015  bnj1097  31049  bnj1110  31050  bnj1118  31052  bnj1128  31058  bnj1125  31060  bnj1145  31061  bnj1136  31065  bnj1173  31070  bnj1189  31077  bnj1204  31080  bnj1279  31086  bnj1321  31095  bnj1413  31103  erdszelem2  31174  cnpconn  31212  cvmscld  31255  mrsubcv  31407  mrsubvr  31408  iprodefisumlem  31626  dvdspw  31636  dfon2lem3  31690  dfon2lem7  31694  frrlem4  31783  nosupfv  31852  nosupres  31853  noetalem1  31863  btwndiff  32134  brcolinear2  32165  btwnconn1  32208  nn0prpwlem  32317  hmeoclda  32328  hmeocldb  32329  ivthALT  32330  fnemeet1  32361  fnejoin1  32363  nnssi3  32455  nndivsub  32456  bj-ceqsalt1  32874  bj-evalidval  33031  onsucuni3  33215  curfv  33389  lindsdom  33403  lindsenlbs  33404  ftc1anclem4  33488  areacirclem2  33501  areacirclem5  33504  areacirc  33505  upixp  33524  filbcmb  33535  cnresima  33563  smprngopr  33851  igenval2  33865  lsmsat  34295  lsmsatcv  34297  lsatcvatlem  34336  islshpcv  34340  l1cvpat  34341  lfli  34348  lshpset2N  34406  cvrnbtwn  34558  meetat2  34584  atcmp  34598  atcvreq0  34601  atlatmstc  34606  cvlcvr1  34626  cvlcvrp  34627  cvlatcvr2  34629  cvr2N  34697  cvratlem  34707  2atjm  34731  athgt  34742  2lplnmN  34845  2llnmj  34846  2lplnmj  34908  dalemswapyzps  34976  dalem23  34982  dalem24  34983  dalem25  34984  dalem27  34985  dalem28  34986  dalem38  34996  dalem39  34997  dalem44  35002  dalem45  35003  dalem51  35009  dalem52  35010  dalem56  35014  pmapglbx  35055  pmapjat1  35139  pmapjat2  35140  paddatclN  35235  osumcllem4N  35245  osumcllem7N  35248  ltrncoval  35431  cdleme0aa  35497  cdleme0b  35499  cdleme8  35537  cdlemesner  35583  cdleme22eALTN  35633  cdleme26eALTN  35649  cdleme35h  35744  cdleme50trn2  35839  cdleme  35848  tgrpov  36036  tendotp  36049  tendoidcl  36057  tendo0co2  36076  cdlemkvcl  36130  dvhopvadd  36382  dvhopellsm  36406  dihmeetlem1N  36579  dihmeetlem9N  36604  dihatexv  36627  lcfl7lem  36788  mapdrvallem2  36934  mapdh9a  37079  hdmapevec  37127  ismrcd1  37261  istopclsd  37263  ismrc  37264  mapfzcons  37279  eldioph2  37325  diophrex  37339  diophren  37377  pellexlem1  37393  pellexlem5  37397  pellqrexplicit  37441  reglogmul  37457  reglogexp  37458  rmxycomplete  37482  congmul  37534  congabseq  37541  acongsym  37543  acongneg2  37544  fzneg  37549  acongeq  37550  jm2.19  37560  jm2.22  37562  jm2.23  37563  jm2.20nn  37564  rmydioph  37581  rmxdiophlem  37582  jm3.1  37587  pwssplit4  37659  hbtlem2  37694  idomrootle  37773  pwinfi2  37867  relexpaddss  38010  trclimalb2  38018  brtrclfv2  38019  trclfvdecomr  38020  ntrclsneine0lem  38362  ntrclsk2  38366  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  gneispace  38432  dvconstbi  38533  expgrowth  38534  chordthmALT  39169  restuni3  39301  wessf1ornlem  39371  disjf1o  39378  elrnmpt2id  39427  funimassd  39431  infnsuprnmpt  39465  infrnmptle  39650  fmul01lt1lem1  39816  climsuselem1  39839  climsuse  39840  limcperiod  39860  lptre2pt  39872  climbddf  39919  limsupvaluz2  39970  supcnvlimsup  39972  cncfshift  40087  cncfperiod  40092  icccncfext  40100  dvnmptconst  40156  dvnprodlem1  40161  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  stoweidlem3  40220  stoweidlem16  40233  stoweidlem17  40234  stoweidlem26  40243  stoweidlem34  40251  stoweidlem57  40274  fourierdlem41  40365  fourierdlem42  40366  fourierdlem52  40375  fourierdlem54  40377  fourierdlem74  40397  fourierdlem75  40398  fourierdlem80  40403  fourierdlem94  40417  fourierdlem102  40425  fourierdlem114  40437  etransclem18  40469  etransclem29  40480  etransclem46  40497  rrxtopnfi  40506  subsaliuncl  40576  sge0f1o  40599  sge0xp  40646  meadjiunlem  40682  voliunsge0lem  40689  volmea  40691  carageniuncllem1  40735  caratheodorylem1  40740  caratheodory  40742  isomenndlem  40744  hoicvr  40762  ovnsubaddlem2  40785  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hspmbllem2  40841  smfaddlem1  40971  smfco  41009  smfsuplem1  41017  2leaddle2  41312  ssfz12  41324  fsumsplitsndif  41343  fsummmodsndifre  41344  fsummmodsnunz  41345  iccpartiltu  41358  icceuelpart  41372  pfxnd  41395  pfxlen0  41396  pfxfv  41399  pfxeq  41404  pfxsuffeqwrdeq  41406  pfxpfx  41415  ccats1pfxeq  41421  ccats1pfxeqrex  41422  pfxccatin12lem2  41424  pfxccatpfx1  41427  pfxccatid  41430  repswpfx  41436  goldbachth  41459  prmdvdsfmtnof1lem1  41496  pwdif  41501  lighneallem1  41522  lighneallem2  41523  lighneallem4a  41525  lighneallem4  41527  lighneal  41528  oexpnegnz  41589  even3prm2  41628  gbepos  41646  gbegt5  41649  gboge9  41652  sbgoldbwt  41665  nnsum3primesgbe  41680  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  tgblthelfgott  41703  tgblthelfgottOLD  41709  sprsymrelfolem2  41743  rngdir  41882  c0snmhm  41915  rngccatidALTV  41989  funcringcsetcALTV2lem6  42041  funcringcsetcALTV2lem9  42044  ringccatidALTV  42052  funcringcsetclem6ALTV  42064  ofaddmndmap  42122  mapprop  42124  nn0sumltlt  42128  gsumpr  42139  domnmsuppn0  42150  scmsuppss  42153  mndpsuppfi  42156  gsumlsscl  42164  ply1ass23l  42170  ply1mulgsumlem1  42174  lincfsuppcl  42202  linccl  42203  lincvalsng  42205  lincvalpr  42207  lincdifsn  42213  ellcoellss  42224  lincext1  42243  lincext2  42244  lincext3  42245  lindslinindimp2lem2  42248  ldepspr  42262  lincresunit3lem1  42268  lincresunit3lem2  42269  islindeps2  42272  logcxp0  42329  elbigo2r  42347  elbigolo1  42351  fllog2  42362  nnolog2flm1  42384  digvalnn0  42393  nn0digval  42394  dignn0fr  42395  dignn0ldlem  42396  dignnld  42397  digexp  42401  dignn0flhalflem1  42409  dignn0flhalflem2  42410  dignn0ehalf  42411  dignn0flhalf  42412  amgmwlem  42548