Theorem ad2antrl 764

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antrl	|- ( ( ch /\ ( ph /\ th ) ) -> ps )

Proof of Theorem ad2antrl

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

Syntax hints:   -> wi 4   /\ wa 384

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

This theorem is referenced by:  simprl  794  simprll  802  simprlr  803  disjxiun  4649  reusv2lem4  4872  fr2nr  5092  somin1  5529  tz7.7  5749  f1oprg  6181  soisores  6577  elovmpt2rab1  6881  sorpssi  6943  onint  6995  ordsucelsuc  7022  elxp5  7111  wemoiso  7153  wemoiso2  7154  el2xptp0  7212  ressuppss  7314  imacosupp  7335  tz7.48lem  7536  oalimcl  7640  oeeui  7682  oaabs2  7725  omabs  7727  swoer  7772  0erOLD  7781  ralxpmap  7907  pw2f1olem  8064  enfixsn  8069  mapxpen  8126  mapunen  8129  unxpdomlem2  8165  unxpdomlem3  8166  findcard3  8203  isfinite2  8218  domunfican  8233  fodomfi  8239  fissuni  8271  fipreima  8272  indexfi  8274  fsuppsssupp  8291  marypha1lem  8339  marypha2  8345  supmo  8358  infmo  8401  oieu  8444  brwdom2  8478  ixpiunwdom  8496  cantnfval2  8566  cantnfle  8568  cantnflt  8569  cantnf  8590  wemapwe  8594  cnfcom  8597  rankonidlem  8691  r1pwcl  8710  infxpenlem  8836  infxpenc2lem1  8842  fseqenlem1  8847  dfac8clem  8855  mappwen  8935  dfac3  8944  dfac5  8951  dfac12lem3  8967  cdainf  9014  infunsdom  9036  coftr  9095  ssfin4  9132  domfin4  9133  fin23lem26  9147  fin23lem22  9149  fin23lem28  9162  fin23lem32  9166  fin23lem40  9173  isf32lem5  9179  compssiso  9196  isf34lem4  9199  isfin1-3  9208  fin1a2lem13  9234  hsmexlem2  9249  hsmexlem4  9251  zorn2lem1  9318  ttukeylem6  9336  iundom2g  9362  konigthlem  9390  pwcfsdom  9405  fpwwe2lem12  9463  fpwwe2  9465  pwfseqlem3  9482  winalim2  9518  r1wunlim  9559  inttsk  9596  inar1  9597  grur1  9642  nqereq  9757  ltexprlem7  9864  prlem936  9869  00id  10211  addid2  10219  ltord1  10554  divdiv1  10736  divdiv2  10737  conjmul  10742  ltdivmul  10898  ledivmul  10899  lt2mul2div  10901  ltdiv23  10914  lediv23  10915  lediv12a  10916  ledivp1  10925  negfi  10971  nn0nndivcl  11362  nn0ge0div  11446  peano2uz2  11465  peano5uzi  11466  eluzp1m1  11711  qbtwnre  12030  xralrple  12036  xleadd1a  12083  xmulge0  12114  xmulass  12117  xlemul1a  12118  iooshf  12252  divelunit  12314  eluzgtdifelfzo  12529  modadd1  12707  modmul1  12723  seqcl2  12819  seqfveq2  12823  seqid2  12847  seqhomo  12848  seqdistr  12852  mulexpz  12900  leexp2r  12918  expnlbnd2  12995  expmulnbnd  12996  hashmap  13222  hashfun  13224  hashbclem  13236  hashfacen  13238  hashf1lem2  13240  hashf1  13241  ccatsymb  13366  swrdsb0eq  13447  swrdswrd  13460  wrdind  13476  wrd2ind  13477  swrdccatin1  13483  swrdccatin2  13487  swrdccatin12  13491  swrdccat  13493  splid  13504  repswswrd  13531  0csh0  13539  2cshw  13559  cshweqrep  13567  relexp0g  13762  relexpsucnnr  13765  relexpindlem  13803  sqrlem1  13983  sqrlem6  13988  rlim  14226  rlimclim1  14276  climsup  14400  caurcvg2  14408  caucvgb  14410  iseralt  14415  sumss  14455  fsum2dlem  14501  mptfzshft  14510  modfsummod  14526  o1fsum  14545  incexclem  14568  divrcnv  14584  flo1  14586  fprodrev  14707  fprod2dlem  14710  ruclem6  14964  moddvds  14991  dvdsaddre2b  15029  dvdsflip  15039  addmodlteqALT  15047  nn0o  15099  fldivndvdslt  15138  bitsf1ocnv  15166  bitsf1  15168  sadcaddlem  15179  bezoutlem2  15257  bezoutlem4  15259  lcmgcdlem  15319  prmind2  15398  isprm5  15419  isprm6  15426  cncongrprm  15437  hashdvds  15480  crth  15483  eulerthlem2  15487  prmdiveq  15491  hashgcdlem  15493  hashgcdeq  15494  iserodd  15540  pclem  15543  pcprendvds2  15546  pcexp  15564  pcneg  15578  pc2dvds  15583  pcmpt  15596  prmpwdvds  15608  pockthg  15610  prmreclem5  15624  4sqlem11  15659  ramub2  15718  ramubcl  15722  ram0  15726  ramub1lem2  15731  ramcl  15733  prmgaplem3  15757  prmgaplem6  15760  setscom  15903  sscpwex  16475  initoeu2  16666  setcinv  16740  funcestrcsetclem9  16788  funcsetcestrclem9  16803  fullsetcestrc  16806  1stfcl  16837  2ndfcl  16838  hofpropd  16907  isacs3lem  17166  isacs4lem  17168  acsmap2d  17179  submnd0  17320  subsubm  17357  frmdup1  17401  frmdup3lem  17403  sgrp2nmndlem2  17411  isgrpinv  17472  subsubg  17617  cycsubgcl  17620  conjghm  17691  qusghm  17697  gsumwrev  17796  symgfixelsi  17855  symgsssg  17887  symgfisg  17888  psgnunilem2  17915  odf1o2  17988  sylow1lem1  18013  odcau  18019  pgpfi  18020  pgpssslw  18029  fislw  18040  efgtlen  18139  efginvrel2  18140  efgrelexlemb  18163  efgredeu  18165  efgcpbllemb  18168  frgpup1  18188  cygabl  18292  lt6abl  18296  gsum2d  18371  gsum2d2lem  18372  gsum2d2  18373  telgsumfzslem  18385  dmdprdsplit2lem  18444  ablfacrp  18465  pgpfac1lem3  18476  gsummgp0  18608  irredrmul  18707  subsubrg  18806  islss4  18962  lspextmo  19056  lspsnat  19145  issubassa  19324  resspsradd  19416  resspsrmul  19417  coe1tmmul2  19646  pf1ind  19719  prmirredlem  19841  znf1o  19900  znidomb  19910  frgpcyg  19922  psgnghm  19926  psgndiflemB  19946  frlmlbs  20136  frlmup1  20137  lindfind  20155  islindf3  20165  lindfmm  20166  mamulid  20247  mat1dimelbas  20277  mdetdiaglem  20404  mdetralt2  20415  mndifsplit  20442  smadiadetglem2  20478  1elcpmat  20520  pmatcollpw3lem  20588  chfacfisf  20659  chfacfisfcpmat  20660  chfacffsupp  20661  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  cayhamlem1  20671  cpmadugsumlemF  20681  cayleyhamilton1  20697  tgcl  20773  pptbas  20812  clsval2  20854  mretopd  20896  lmbr2  21063  cncls2  21077  nrmsep  21161  regsep2  21180  cmpsublem  21202  cmpsub  21203  tgcmp  21204  uncmp  21206  hauscmplem  21209  iunconnlem  21230  1stcrest  21256  2ndcctbss  21258  2ndcsep  21262  dis2ndc  21263  hausllycmp  21297  dislly  21300  kgentopon  21341  1stckgen  21357  kgencn3  21361  ptpjpre1  21374  ptbasin  21380  ptpjopn  21415  dfac14  21421  ptcnplem  21424  txcn  21429  txindis  21437  txdis1cn  21438  ptrescn  21442  txcmplem1  21444  txcmp  21446  txhaus  21450  txlm  21451  tx1stc  21453  txkgen  21455  xkococn  21463  qtopcn  21517  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  hmeoimaf1o  21573  reghmph  21596  nrmhmph  21597  txhmeo  21606  ptuncnv  21610  filconn  21687  fbasrn  21688  fmfnfmlem2  21759  flimfnfcls  21832  cnpfcfi  21844  alexsublem  21848  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem3  21858  cnextfval  21866  tsmsxp  21958  imasdsf1olem  22178  bl2in  22205  blssps  22229  blss  22230  blssexps  22231  blssex  22232  blcld  22310  stdbdxmet  22320  met1stc  22326  prdsxmslem2  22334  metcnp3  22345  metcnpi3  22351  txmetcnp  22352  nmo0  22539  nmoid  22546  icccmplem1  22625  icccmp  22628  xrge0tsms  22637  metdseq0  22657  cnheiborlem  22753  cnheibor  22754  cnllycmp  22755  pcoval2  22816  cmetcaulem  23086  iscmet3lem1  23089  iscmet3lem2  23090  equivcau  23098  lmcau  23111  cncmet  23119  ivthlem2  23221  ivthlem3  23222  ovoliunlem2  23271  ovolscalem2  23282  uniioombl  23357  dyaddisj  23364  opnmbllem  23369  volivth  23375  ismbfd  23407  ismbf3d  23421  mbfimaopnlem  23422  mbfinf  23432  itg1addlem4  23466  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2seq  23509  itg2lea  23511  itg2split  23516  itg2cnlem1  23528  limciun  23658  dvmptfsum  23738  rolle  23753  c1lip1  23760  dvcnvrelem1  23780  dvcnvre  23782  dvcvx  23783  itgsubst  23812  tdeglem4  23820  mdegmullem  23838  plyco0  23948  coemullem  24006  dgreq0  24021  dgrmul  24026  dgrco  24031  elqaalem2  24075  aannenlem1  24083  aaliou3lem9  24105  ulmres  24142  ulmshftlem  24143  angneg  24533  dcubic  24573  cxploglim  24704  cxploglim2  24705  scvxcvx  24712  lgamgulmlem5  24759  lgamcvg2  24781  basellem3  24809  basellem4  24810  sqff1o  24908  fsumdvdsdiaglem  24909  dvdsflsumcom  24914  dvdsmulf1o  24920  fsumvma2  24939  logfac2  24942  logfacrlim  24949  logexprlim  24950  dchrelbasd  24964  lgsne0  25060  lgsqrlem2  25072  lgsqrmodndvds  25078  gausslemma2dlem1a  25090  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem2  25110  2sqlem8  25151  2sqlem11  25154  chpo1ubb  25170  vmadivsum  25171  rplogsumlem2  25174  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasumlem1  25184  dchrisum0fno1  25200  dchrisum0re  25202  dchrisum0lem1  25205  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrisum0  25209  mulogsumlem  25220  mulog2sumlem2  25224  vmalogdivsum2  25227  logsqvma  25231  log2sumbnd  25233  selberglem3  25236  selberg  25237  selberg2lem  25239  selberg2b  25241  selberg3lem2  25247  pntrmax  25253  pntrsumo1  25254  pntlemn  25289  pntlemp  25299  qabvle  25314  ostthlem1  25316  ostthlem2  25317  ostth2lem2  25323  ostth3  25327  idmot  25432  iscgra1  25702  brbtwn2  25785  colinearalglem4  25789  colinearalg  25790  ax5seglem9  25817  axpaschlem  25820  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  eengtrkg  25865  upgr1eopALT  26012  uspgredg2vlem  26115  subumgr  26180  edgnbusgreu  26269  nb3grprlem1  26282  wlkl1loop  26534  pthdivtx  26625  usgr2pth  26660  crctcshwlkn0  26713  wlklnwwlkln1  26754  wwlksnext  26788  clwlkclwwlklem2a  26899  clwwlkinwwlk  26905  clwwlksf  26915  wwlksubclwwlks  26925  clwwnisshclwwsn  26930  clwwlksnscsh  26940  1conngr  27054  n4cyclfrgr  27155  numclwlk1lem2f1  27227  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwwlk7  27249  frgrogt3nreg  27255  grpoidinvlem1  27358  grpoidinvlem3  27360  grporcan  27372  nmlnoubi  27651  blocnilem  27659  ipblnfi  27711  htthlem  27774  ocsh  28142  shmodsi  28248  pjhthlem2  28251  5oalem2  28514  eigposi  28695  nmopub2tALT  28768  nmfnleub2  28785  nmcexi  28885  nmopcoi  28954  kbass3  28977  mdslmd1lem1  29184  mdslmd1lem2  29185  chirredlem2  29250  chirredlem4  29252  mdsymlem3  29264  mdsymlem5  29266  sumdmdii  29274  sumdmdlem  29277  sumdmdlem2  29278  foresf1o  29343  disjxpin  29401  1stpreimas  29483  resf1o  29505  gsumvsca1  29782  gsumvsca2  29783  xrge0tsmsd  29785  mdetpmtr1  29889  mdetpmtr2  29890  pstmxmet  29940  qqhghm  30032  qqhrhm  30033  esumpcvgval  30140  volmeas  30294  imambfm  30324  dya2iocnrect  30343  oddpwdc  30416  sseqf  30454  orvcgteel  30529  orvclteel  30534  ballotlemsf1o  30575  bnj1110  31050  bnj1118  31052  txpconn  31214  connpconn  31217  cnllysconn  31227  rellysconn  31233  cvmsss2  31256  cvmlift2lem9  31293  mrsubfval  31405  mppsval  31469  dfon2lem6  31693  trpredmintr  31731  wzel  31771  wzelOLD  31772  sltres  31815  nosupno  31849  nosupbnd2  31862  sslttr  31914  ifscgr  32151  cgrxfr  32162  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem12  32205  brsegle  32215  finminlem  32312  gtinfOLD  32314  nn0prpwlem  32317  fnessref  32352  refssfne  32353  neibastop1  32354  topjoin  32360  fnemeet2  32362  bj-finsumval0  33147  topdifinffinlem  33195  matunitlindflem2  33406  poimirlem28  33437  poimirlem32  33441  opnmbllem0  33445  mblfinlem1  33446  mblfinlem4  33449  ismblfin  33450  mbfresfi  33456  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  bddiblnc  33480  unirep  33507  frinfm  33530  sdclem2  33538  geomcau  33555  istotbnd3  33570  sstotbnd2  33573  sstotbnd  33574  sstotbnd3  33575  totbndbnd  33588  cntotbnd  33595  ismtyres  33607  heibor1lem  33608  heiborlem1  33610  heiborlem8  33617  ismndo1  33672  isdivrngo  33749  unichnidl  33830  cvlcvr1  34626  ishlat3N  34641  llnmlplnN  34825  islvol2aN  34878  4atlem4c  34887  4atlem4d  34888  isline2  35060  isline3  35062  linepsubclN  35237  lhpexle3lem  35297  lhpjat2  35307  cdlemd4  35488  cdleme0cq  35502  cdleme32fva  35725  cdleme32fvaw  35727  tendo0mul  36114  tendo0mulr  36115  diameetN  36345  dvhvaddcl  36384  dvhvaddcomN  36385  cdlemm10N  36407  dvadiaN  36417  djavalN  36424  dihvalcqat  36528  dihopelvalcpre  36537  djhval  36687  dihjat1lem  36717  elrfi  37257  nacsfix  37275  fzsplit1nn0  37317  eldioph2  37325  lzenom  37333  irrapxlem3  37388  pellexlem5  37397  pell1234qrne0  37417  pell1234qrmulcl  37419  pell14qrdich  37433  pell1qrge1  37434  pellqrex  37443  reglogltb  37455  reglogleb  37456  rmxypairf1o  37476  rmxycomplete  37482  monotoddzzfi  37507  congadd  37533  congsym  37535  acongrep  37547  jm2.19lem3  37558  jm2.19lem4  37559  jm2.22  37562  jm2.25  37566  expdiophlem1  37588  wepwsolem  37612  kelac1  37633  lmhmfgsplit  37656  pwslnm  37664  hbtlem6  37699  hbt  37700  mon1psubm  37784  deg1mhm  37785  iunrelexp0  37994  dssmapnvod  38314  gsumws3  38499  gsumws4  38500  mulltgt0  39181  fnchoice  39188  disjrnmpt2  39375  fzisoeu  39514  fsumiunss  39807  climinf  39838  mullimc  39848  mullimcf  39855  stoweidlem14  40231  stoweidlem17  40234  stoweidlem34  40251  stoweidlem50  40267  fourierdlem42  40366  fourierdlem62  40385  fourierdlem71  40394  fourierdlem76  40399  qndenserrnbllem  40514  subsaliuncl  40576  sge0resplit  40623  iccpartigtl  41359  ccatpfx  41409  pfxccatin12lem2  41424  pfxccatin12  41425  prmdvdsfmtnof1lem2  41497  bgoldbtbndlem3  41695  bgoldbtbnd  41697  uspgrsprf1  41755  subsubmgm  41797  isassintop  41846  2zlidl  41934  2zrngnmrid  41950  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  funcringcsetcALTV2lem9  42044  ringcinvALTV  42056  funcringcsetclem9ALTV  42067  fldhmsubc  42084  fldhmsubcALTV  42102  mndpsuppss  42152  gsumlsscl  42164  lincsum  42218  lindslinindsimp1  42246  lindslinindimp2lem4  42250  lincresunitlem2  42265  elfzolborelfzop1  42309  elbigo2  42346  digexp  42401  dig1  42402  nn0sumshdiglemB  42414