Theorem 3adant2 1080

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

Step	Hyp	Ref	Expression
1		3simpb 1059	. 2 |- ( ( ph /\ th /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 17	1 |- ( ( ph /\ th /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384   /\ 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:  3ad2ant1  1082  eupickb  2538  vtoclegft  3280  eqeu  3377  funopg  5922  fnco  5999  dff1o2  6142  fnimapr  6262  fvmptt  6300  fnreseql  6327  f1elima  6520  f13dfv  6530  f1ocnvfvb  6535  oprssov  6803  ordunel  7027  poxp  7289  wfrlem4  7418  smoiso  7459  oaord  7627  oaword  7629  omcan  7649  omwordri  7652  odi  7659  omeulem1  7662  oeord  7668  oecan  7669  oewordri  7672  oeordsuc  7674  nnaord  7699  nnaordr  7700  nndi  7703  nnaword  7707  nnmwordri  7716  erov  7844  ecopovtrn  7850  xpdom3  8058  mapxpen  8126  findcard  8199  indexfi  8274  suppr  8377  infpr  8409  r111  8638  tcrank  8747  acndom  8874  infdif2  9032  infxpdom  9033  cfeq0  9078  cfsuc  9079  cfflb  9081  cflim2  9085  cfsmolem  9092  axcc3  9260  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  pwcfsdom  9405  tsktrss  9583  tsksuc  9584  tskuni  9605  adderpqlem  9776  mulerpqlem  9777  mulcanenq  9782  distrnq  9783  ltsonq  9791  ltanq  9793  ltmnq  9794  distrlem1pr  9847  distrlem5pr  9849  ltsopr  9854  ltsosr  9915  ltasr  9921  adddir  10031  axlttrn  10110  letr  10131  nnncan1  10317  npncan3  10319  pnpcan2  10321  subdi  10463  subdir  10464  mulcan1g  10680  mulcan2g  10681  divmul  10688  div23  10704  div13  10706  muldivdir  10720  divsubdir  10721  divcan7  10734  ltmul2  10874  lemul1  10875  lemul2  10876  lemul2a  10878  lediv1  10888  ltmuldiv2  10897  lemuldiv  10903  lemuldiv2  10904  ltdiv2  10909  lediv2  10913  fiminre  10972  infrelb  11008  nndivtr  11062  bndndx  11291  nn0n0n1ge2  11358  fnn0ind  11476  addlelt  11942  xrletr  11989  qsqueeze  12032  xleadd2a  12084  xleadd1  12085  xltadd2  12087  xltmul2  12123  supxrbnd  12158  iooneg  12292  iccneg  12293  icoshft  12294  icoshftf1o  12295  zltaddlt1le  12324  fzen  12358  uzsubsubfz  12363  ssfzunsnext  12386  fzrevral2  12426  fzshftral  12428  fz0fzdiffz0  12448  elfzmlbp  12450  elfzo  12472  nelfzo  12475  fzoaddel2  12523  fzosubel2  12527  elfzom1p1elfzo  12547  ssfzo12bi  12563  fzonfzoufzol  12571  subfzo0  12590  flltdivnn0lt  12634  modmulnn  12688  modcyc  12705  modaddabs  12708  modaddmod  12709  modmuladd  12712  modadd2mod  12720  modsubmod  12728  modsubmodmod  12729  modaddmodup  12733  modmulmod  12735  moddi  12738  modsubdir  12739  modfzo0difsn  12742  modsumfzodifsn  12743  uzindi  12781  axdc4uzlem  12782  expneg2  12869  expdiv  12911  expubnd  12921  mulbinom2  12984  bernneq2  12991  hashinfxadd  13174  brfi1indlem  13278  ccatval3  13363  ccatsymb  13366  ccatfv0  13367  ccatval1lsw  13368  ccats1val2  13404  swrdnd  13432  2swrd1eqwrdeq  13454  swrdswrd  13460  wrd2ind  13477  swrdccatin1  13483  swrdccatin12lem2b  13486  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccat  13493  swrdccat3a  13494  swrdccat3blem  13495  repswswrd  13531  repswccat  13532  cshwidxmod  13549  2cshw  13559  3cshw  13564  scshwfzeqfzo  13572  cshwcsh2id  13574  cshimadifsn  13575  cshimadifsn0  13576  ccatco  13581  cshco  13582  swrdco  13583  lswco  13584  swrds2  13685  2swrd2eqwrdeq  13696  shftuz  13809  shftval2  13815  abs3dif  14071  fsumdifsnconst  14523  modfsummods  14525  sin02gt0  14922  dvdsval2  14986  dvdscmul  15008  dvdsmulc  15009  dvdscmulr  15010  dvdsmulcr  15011  mulmoddvds  15051  divalglem8  15123  ndvdssub  15133  rpmulgcd  15275  coprmdvdsOLD  15367  coprmprod  15375  cncongr1  15381  cncongr2  15382  isprm3  15396  modprm0  15510  coprimeprodsq  15513  pythagtriplem12  15531  pythagtriplem14  15533  pcprendvds  15545  pcmul  15556  pcdiv  15557  pcqcl  15561  pcqdiv  15562  pcdvdsb  15573  pcgcd  15582  vdwnnlem1  15699  hashbcss  15708  cshwshashlem1  15802  fvsetsid  15890  setsstruct2  15896  setsstruct  15898  mrcss  16276  mrcsscl  16280  mrcun  16282  cofulid  16550  catcisolem  16756  funcsetcestrclem9  16803  latleeqj1  17063  lubun  17123  clatleglb  17126  pslem  17206  dirtr  17236  mgmb1mgm1  17254  pwspjmhm  17368  gsumccat  17378  grpinvid1  17470  grpinvid2  17471  grpasscan1  17478  grpasscan2  17479  grpinvadd  17493  grpsubf  17494  grpsubrcan  17496  grpinvsub  17497  grpsubeq0  17501  grpsubadd0sub  17502  grppncan  17506  grpnpcan  17507  mulgnn0p1  17552  mulgaddcomlem  17563  mulginvcom  17565  mulginvinv  17566  subgsubcl  17605  subgsub  17606  eqglact  17645  qussub  17654  ghmsub  17668  psgnunilem4  17917  oddvds2  17983  odsubdvds  17986  gexnnod  18003  slwn0  18030  gsumdixp  18609  dvrcl  18686  unitdvcl  18687  dvrcan1  18691  dvrcan3  18692  dvreq1  18693  subrgdv  18797  abvsubtri  18835  idsrngd  18862  lmodvsubval2  18918  lsmcl  19083  lsmsp2  19087  lspsntrim  19098  lidldvgen  19255  evlslem4  19508  mpfsubrg  19532  ply1tmcl  19642  eqcoe1ply1eq  19667  gsummoncoe1  19674  lply1binomsc  19677  chrcong  19877  zndvds  19898  zntoslem  19905  ocvsscon  20019  obselocv  20072  frlmphl  20120  mamudm  20194  mamufacex  20195  scmatf1  20337  scmatf1o  20338  scmatrngiso  20342  submabas  20384  mdetdiaglem  20404  mdetralt2  20415  mdetero  20416  mdetunilem2  20419  mdetunilem6  20423  m2detleiblem7  20433  maducoeval2  20446  gsummatr01lem3  20463  gsummatr01  20465  smadiadetglem2  20478  cramerlem1  20493  mply1topmatcl  20610  mp2pm2mplem4  20614  ntrin  20865  elnei  20915  neindisj2  20927  ordtopn3  21000  ordtcld3  21003  leordtval2  21016  lecldbas  21023  cnrest2  21090  cmpsublem  21202  ptrescn  21442  xkococn  21463  kqfeq  21527  snfbas  21670  neifil  21684  fclsrest  21828  utopsnnei  22053  neipcfilu  22100  psmetsym  22115  psmetge0  22117  xmetge0  22149  xmetsym  22152  metustto  22358  metustbl  22371  restmetu  22375  nm2dif  22429  nmtri  22430  cnmet  22575  cnmpt2pc  22727  iihalf1  22730  iihalf2  22732  iocopnst  22739  clmnegsubdi2  22905  clmsub4  22906  clmvsubval2  22910  ncvspi  22956  cphsqrtcl3  22987  cph2ass  23013  cphipval2  23040  cphipval  23042  caublcls  23107  bcthlem3  23123  bcthlem4  23124  srabn  23156  rrxmet  23191  iblconst  23584  tdeglem3  23819  mdegmullem  23838  dvdsq1p  23920  coeid3  23996  aannenlem2  24084  pserdvlem2  24182  tanord1  24283  cxpef  24411  recxpcl  24421  logbchbase  24509  relogbcl  24511  relogbzcl  24512  logbleb  24521  logblt  24522  relogbcxpb  24525  lawcos  24546  pythag  24547  isosctrlem1  24548  isosctrlem2  24549  lgsmodeq  25067  lgsmulsqcoprm  25068  gausslemma2dlem1a  25090  2lgsoddprmlem2  25134  ax5seglem1  25808  axcontlem2  25845  axcontlem8  25851  upgrpredgv  26034  numedglnl  26039  issubgr2  26164  uhgrissubgr  26167  egrsubgr  26169  fusgrfisstep  26221  nbusgrfi  26276  nb3grprlem2  26283  cplgr3v  26331  cusgrsizeindslem  26347  finsumvtxdg2size  26446  rusgrpropadjvtx  26481  upgrwlkvtxedg  26541  usgr2trlncl  26656  uspgrn2crct  26700  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  wwlksnextproplem3  26806  umgr2adedgwlklem  26840  rusgr0edg  26868  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwwlks1loop  26908  clwwlksn1loop  26909  clwwlksel  26914  clwwisshclwwslemlem  26926  erclwwlkstr  26936  erclwwlksntr  26948  clwlksfclwwlk  26962  uhgr3cyclex  27042  umgr3cyclex  27043  eucrctshift  27103  frgr3v  27139  3cyclfrgrrn  27150  frgrwopreglem5a  27175  numclwlk3lem3  27206  numclwwlkovf2exlem2  27212  extwwlkfab  27223  numclwwlk5  27246  numclwwlk6  27248  isgrpo  27351  grpoinvid1  27382  grpoinvid2  27383  grpoinvop  27387  grpodivinv  27390  grpoinvdiv  27391  grpodivf  27392  grponpcan  27397  ablonncan  27411  nvmval  27497  nvmval2  27498  nvmfval  27499  nvmul0or  27505  nvpncan2  27508  nvaddsub4  27512  nvmeq0  27513  nvdif  27521  nvpi  27522  nvmtri  27526  nvabs  27527  imsmetlem  27545  ipval2lem3  27560  ipval2  27562  4ipval2  27563  ipval3  27564  nmooge0  27622  blometi  27658  hvaddsub12  27895  hvsubdistr1  27906  hvsubdistr2  27907  hvaddcan2  27928  hvmulcan  27929  hvmulcan2  27930  hvsubcan  27931  hvsubcan2  27932  his7  27947  his2sub  27949  his2sub2  27950  norm3dif2  28008  shsubcl  28077  hhssnv  28121  shlej2  28220  fh2  28478  cm2j  28479  pjoi0  28576  hodcl  28606  hosubdi  28667  unopf1o  28775  unopadj  28778  adj2  28793  braadd  28804  bramul  28805  lnopaddmuli  28832  lnopsubmuli  28834  homco2  28836  lnfnaddmuli  28904  adjlnop  28945  leopmul  28993  leoptr  28996  pjimai  29035  atcv1  29239  atexch  29240  atcvatlem  29244  fcoinvbr  29419  divnumden2  29564  xdivmul  29633  resvsca  29830  hasheuni  30147  difelsiga  30196  cndprobin  30496  bayesth  30501  sgn3da  30603  breprexplemc  30710  lediv2aALT  31571  subdivcomb1  31611  fununiq  31667  dfrdg2  31701  sltres  31815  sletr  31883  clsun  32323  neiin  32327  rdgeqoa  33218  curfv  33389  matunitlindflem1  33405  poimirlem32  33441  ftc1anclem4  33488  areacirc  33505  filbcmb  33535  ismtybnd  33606  grpoeqdivid  33680  ghomco  33690  rngonegrmul  33743  zerdivemp1x  33746  rngohomco  33773  rngoisoco  33781  riscer  33787  intidl  33828  isfldidl  33867  lshpnelb  34271  opnlen0  34475  opcon3b  34483  opcon2b  34484  oplecon3b  34487  opltcon3b  34491  opltcon2b  34493  oldmm1  34504  oldmm4  34507  oldmj1  34508  oldmj4  34511  cvrval2  34561  cvrcon3b  34564  leatb  34579  atcmp  34598  atcvreq0  34601  atlatle  34607  athgt  34742  3dim2  34754  islln2a  34803  lplnnleat  34828  lvolnleat  34869  4atlem10  34892  4atlem11  34895  4atlem12  34898  dalem21  34980  dalem22  34981  dalem23  34982  dalem29  34987  dalem30  34988  dalem31N  34989  dalem32  34990  dalem33  34991  dalem34  34992  dalem35  34993  dalem36  34994  dalem37  34995  dalem40  34998  dalem46  35004  dalem47  35005  dalem51  35009  dalem52  35010  dalem58  35016  dalem59  35017  pmaple  35047  paddclN  35128  pmapjoin  35138  pmapjat1  35139  elpcliN  35179  pclssN  35180  pclun2N  35185  2polcon4bN  35204  paddunN  35213  poldmj1N  35214  pmapj2N  35215  pmapocjN  35216  psubclinN  35234  paddatclN  35235  poml4N  35239  lautco  35383  ldilco  35402  ltrneq2  35434  trljat1  35453  cdlemc1  35478  cdleme10  35541  ltrnco  36007  trlcocnv  36008  trljco  36028  trljco2  36029  cdlemi1  36106  tendocnv  36310  diaord  36336  dibord  36448  dihord3  36546  dihord4  36547  dihmeetlem2N  36588  dihmeetlem4preN  36595  dochdmj1  36679  hdmap10lem  37131  mzprename  37312  dvdsrabdioph  37374  pell14qrdivcl  37429  monotoddzz  37508  jm2.19lem2  37557  jm2.19  37560  relexpaddss  38010  k0004lem3  38447  dvconstbi  38533  chordthmALT  39169  isosctrlem1ALT  39170  ssinc  39264  ssdec  39265  unima  39346  wessf1ornlem  39371  disjf1o  39378  disjinfi  39380  ssnnf1octb  39382  projf1o  39386  mapsnd  39388  mapssbi  39405  iunmapsn  39409  fvelimad  39458  upbdrech  39519  iuneqfzuzlem  39550  suplesup  39555  rexabslelem  39645  climxrrelem  39981  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  cncfshift  40087  cncfperiod  40092  cncfuni  40099  icccncfext  40100  dvmptfprodlem  40159  dvnprodlem1  40161  itgspltprt  40195  ismbl3  40203  stoweidlem3  40220  stoweidlem10  40227  stoweidlem19  40236  stoweidlem31  40248  stoweidlem34  40251  stoweidlem44  40261  fourierdlem41  40365  fourierdlem42  40366  fourierdlem51  40374  fourierdlem68  40391  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  fourierdlem94  40417  etransclem24  40475  etransclem34  40485  rrxdsfi  40505  qndenserrnbllem  40514  salincl  40543  saldifcl2  40546  subsalsal  40577  sge0pr  40611  sge0pnffigt  40613  sge0reuz  40664  nnfoctbdjlem  40672  nnfoctbdj  40673  meadjiunlem  40682  caratheodorylem2  40741  hoidmv1le  40808  hoidmvlelem3  40811  hspmbllem2  40841  opnvonmbllem2  40847  sssmf  40947  smfaddlem1  40971  sigaraf  41042  sigarmf  41043  nltle2tri  41323  subsubelfzo0  41336  iccpartiltu  41358  icceuelpart  41372  pfxsuffeqwrdeq  41406  pfxsuff1eqwrdeq  41407  ccatpfx  41409  pfxpfx  41415  pfxccatin12lem1  41423  pfxccatpfx1  41427  pfxccatpfx2  41428  repswpfx  41436  pfxco  41438  proththd  41531  mogoldbblem  41629  bgoldbtbndlem2  41694  xpprsng  42110  nn0sumltlt  42128  invginvrid  42148  ply1sclrmsm  42171  linccl  42203  lincvalpr  42207  lincresunit3lem1  42268  lincresunit3  42270  fdivmpt  42334  nnolog2flm1  42384  dignnld  42397  digexp  42401  dignn0flhalflem1  42409  setrec2fun  42439  reccot  42499  rectan  42500