Theorem adantll 711

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantll	⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		simpr 485	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 580	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad2antlr  724  ad2ant2l  743  ad2ant2lr  745  ad5ant23  757  ad5ant24  758  ad5ant25  759  3adant1  1129  3ad2antl3  1186  ralcom2  3291  ralimda  3432  vtocl2d  3497  sbc2iegf  3799  sbcralt  3806  pofun  5522  poinxp  5668  xpdifid  6076  sossfld  6094  preddowncl  6239  tz7.7  6296  onfr  6309  ssimaex  6862  fndmdif  6928  dffo4  6988  fcompt  7014  fconst2g  7087  f1cofveqaeq  7140  2f1fvneq  7142  isores3  7215  fvmptopabOLD  7339  limsssuc  7706  el2mpocl  7935  1stconst  7949  2ndconst  7950  curry1  7953  curry2  7956  extmptsuppeq  8013  suppss  8019  suppssOLD  8020  suppssov1  8023  suppss2  8025  onnseq  8184  oe0  8361  oesuclem  8364  oecl  8376  oaordi  8386  oawordri  8390  omordi  8406  omword2  8414  omlimcl  8418  odi  8419  omass  8420  oeoe  8439  nnaordi  8458  oaabs  8487  omsmolem  8496  eceqoveq  8620  mapsnd  8683  dom2lem  8789  sbthlem9  8887  php3OLD  9016  onomeneqOLD  9021  isinf  9045  frfi  9068  fiint  9100  fodomfib  9102  fofinf1o  9103  marypha1lem  9201  ordiso2  9283  unwdomg  9352  xpwdomg  9353  frr1  9526  ac5num  9801  cff1  10023  cfcoflem  10037  infpssrlem4  10071  isf32lem9  10126  isf34lem7  10144  fin1a2lem13  10177  fin1a2s  10179  hsmexlem4  10194  axdc2lem  10213  zorn2lem6  10266  axpowndlem2  10363  inttsk  10539  tskuni  10548  nqereu  10694  prcdnq  10758  addclprlem2  10782  ltexpri  10808  prlem936  10812  reclem2pr  10813  axsup  11059  add4  11204  ltleadd  11467  lt2mul2div  11862  nn2ge  12009  zextle  12402  fnn0ind  12428  xrlttr  12883  ifle  12940  xnn0lem1lt  12987  xaddass  12992  xmulasslem3  13029  xlemul1a  13031  xadddilem  13037  xrsupsslem  13050  xrinfmsslem  13051  supxrunb1  13062  supxrunb2  13063  ixxin  13105  difreicc  13225  iccsplit  13226  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  fzaddel  13299  fzadd2  13300  fzrev  13328  modadd1  13637  modmul1  13653  fsuppmapnn0fiub  13720  mulexp  13831  expadd  13834  expmul  13837  expnbnd  13956  bccl  14045  hashdom  14103  prsshashgt1  14134  hashfacen  14175  hashfacenOLD  14176  brfi1uzind  14221  wrdnval  14257  swrdccat3blem  14461  revccat  14488  2shfti  14800  rexico  15074  cau3lem  15075  subcn2  15313  caucvgb  15400  iseraltlem1  15402  sumss  15445  fsumsplitsn  15465  incexclem  15557  supcvg  15577  mertenslem2  15606  fprodn0  15698  fprodsplitsn  15708  fprodle  15715  eftlcl  15825  reeftlcl  15826  rpnnen2lem6  15937  dvdsext  16039  3dvds  16049  sqoddm1div8z  16072  gcdcllem3  16217  bezoutr1  16283  seq1st  16285  dvdslcm  16312  lcmeq0  16314  lcmcl  16315  lcmneg  16317  lcmdvds  16322  coprmgcdb  16363  dvdsprime  16401  pc2dvds  16589  prmpwdvds  16614  unbenlem  16618  infpnlem1  16620  1arith  16637  vdwmc2  16689  ramcl  16739  mrcuni  17339  isacs1i  17375  acsfn  17377  funcpropd  17625  curfcl  17959  curf2ndf  17974  resmhm  18468  resmhm2b  18470  mhmco  18471  mhmima  18472  pwsdiagmhm  18478  gsumwsubmcl  18484  gsumwspan  18494  pwmnd  18585  dfgrp2  18613  subgint  18788  ghmmhmb  18854  resghm  18859  cntzmhm  18954  symgextf1lem  19037  f1omvdconj  19063  dfod2  19180  gexdvds  19198  subgpgp  19211  sylow1lem3  19214  frgpnabllem1  19483  dprdfeq0  19634  isdrng2  20010  cntzsubr  20066  islmodd  20138  lsslss  20232  reslmhm2b  20325  psgnfix1  20812  psgndif  20816  copsgndif  20817  ocvocv  20885  frlmsslsp  21012  frlmlbs  21013  psrbaglefi  21144  psrbaglefiOLD  21145  mptcoe1fsupp  21395  psropprmul  21418  ply1coe  21476  mamudi  21559  mamudir  21560  mat1dimelbas  21629  scmatmulcl  21676  scmatfo  21688  mulmarep1gsum2  21732  mdetunilem7  21776  mdetunilem9  21778  gsummatr01lem3  21815  smadiadetlem3  21826  cpmadugsumlemF  22034  leordtval  22373  cnpnei  22424  cnco  22426  cnss1  22436  cmpsub  22560  hauscmplem  22566  dissnlocfin  22689  ptbasid  22735  tx2cn  22770  upxp  22783  txindis  22794  xkoptsub  22814  xkopt  22815  trfbas2  23003  filconn  23043  trfil2  23047  filssufilg  23071  ufileu  23079  fixufil  23082  ufilen  23090  rnelfmlem  23112  flimclsi  23138  hauspwpwf1  23147  fclsopn  23174  fclsfnflim  23187  fclscmpi  23189  alexsubALTlem4  23210  ptcmplem5  23216  tgpmulg  23253  subgtgp  23265  tgpt0  23279  tsmsxplem2  23314  metss  23673  metustfbas  23722  dscopn  23738  xrsmopn  23984  cncfss  24071  icoopnst  24111  iccpnfcnv  24116  icccvx  24122  evth  24131  phtpycc  24163  pcohtpylem  24191  lmmbrf  24435  fgcfil  24444  caucfil  24456  cfilres  24469  bcth3  24504  cmscsscms  24546  ovolfioo  24640  ovolficc  24641  voliunlem3  24725  volcn  24779  mbflimsup  24839  mbfi1fseqlem5  24893  itg2seq  24916  bddiblnc  25015  dvnff  25096  dvnadd  25102  cpnord  25108  c1liplem1  25169  plypf1  25382  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  coeidlem  25407  dgrle  25413  dgrnznn  25417  plycjlem  25446  elqaalem3  25490  ulmcaulem  25562  ulmcau  25563  psergf  25580  psercn2  25591  efopn  25822  abscxpbnd  25915  leibpi  26101  isppw2  26273  muinv  26351  bposlem3  26443  gausslemma2dlem4  26526  pntrmax  26721  pntpbnd1  26743  qabvexp  26783  eqeelen  27281  colinearalglem4  27286  axcgrid  27293  axsegconlem1  27294  axsegconlem3  27296  ax5seglem1  27305  ax5seglem2  27306  ax5seglem9  27314  axcontlem2  27342  cusgrfilem2  27832  vtxdgfisf  27852  usgr2pthlem  28140  uspgrn2crct  28182  crctcshwlkn0  28195  wwlksnext  28267  wwlksnextproplem3  28285  eupth2lem3lem4  28604  frgr3vlem1  28646  frgr3vlem2  28647  3vfriswmgrlem  28650  frgrwopreglem5  28694  numclwwlk3lem2  28757  grpoidinvlem3  28877  grpoidinv  28879  grpoideu  28880  nmoub3i  29144  nmlno0lem  29164  nmlnoubi  29167  ipasslem3  29204  ipblnfi  29226  hvaddsub4  29449  his35  29459  shsel3  29686  chj4  29906  spansncol  29939  chscllem2  30009  5oalem2  30026  3oalem2  30034  hoaddcl  30129  adjsym  30204  cnvadj  30263  hhcno  30275  hhcnf  30276  nmopub2tALT  30280  unoplin  30291  counop  30292  nmfnleub2  30297  hmoplin  30313  brafnmul  30322  nmlnop0iALT  30366  nmopun  30385  nmophmi  30402  riesz3i  30433  riesz1  30436  cnlnadjlem2  30439  cnlnadjlem6  30443  adjmul  30463  adjadd  30464  bra11  30479  cnvbraval  30481  kbass5  30491  kbass6  30492  leop2  30495  leopadd  30503  leopmuli  30504  leoptri  30507  leopnmid  30509  nmopleid  30510  pj3si  30578  hstel2  30590  cvcon3  30655  dmdmd  30671  dmdbr5  30679  mdsl0  30681  mdslmd1lem1  30696  mdslmd1lem2  30697  mdslmd3i  30703  superpos  30725  chirredlem2  30762  chirredlem3  30763  mdsymlem3  30776  mdsymlem5  30778  mdsymlem6  30779  sumdmdlem  30789  cdjreui  30803  cdj1i  30804  cdj3i  30812  foresf1o  30859  2ndimaxp  30993  abfmpel  31001  fcomptf  31004  fcnvgreu  31019  fdifsuppconst  31032  xrge0infss  31092  xnn0gt0  31101  cycpm2tr  31395  intlidl  31611  rhmpreimaprmidl  31636  lssdimle  31700  mdetpmtr1  31782  cmpcref  31809  xrge0iifcnv  31892  esumcst  32040  hasheuni  32062  esum2dlem  32069  esum2d  32070  sigaclcu2  32097  insiga  32114  unelldsys  32135  measres  32199  measdivcst  32201  volfiniune  32207  ddemeas  32213  sgn3da  32517  actfunsnf1o  32593  fnrelpredd  33070  fineqvac  33075  sconnpi1  33210  cvmsss2  33245  satfv1lem  33333  fmlaomn0  33361  gonarlem  33365  mrsubco  33492  dfon2lem6  33773  poseq  33811  soseq  33812  madebday  34089  hfext  34494  elicc3  34515  fnessref  34555  bj-ismooredr2  35290  pibt2  35597  fin2solem  35772  fin2so  35773  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem2  35788  poimirlem14  35800  poimirlem25  35811  poimirlem26  35812  poimirlem29  35815  poimirlem30  35816  broucube  35820  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ex-ovoliunnfl  35829  mbfresfi  35832  cnambfre  35834  itg2addnclem  35837  itg2addnclem2  35838  itg2addnc  35840  ftc1anclem3  35861  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  eqfnun  35889  indexdom  35901  filbcmb  35907  fdc  35912  incsequz  35915  metf1o  35922  caures  35927  bndss  35953  ismtycnv  35969  heiborlem1  35978  rrncmslem  35999  isdrngo2  36125  rngoisocnv  36148  unichnidl  36198  erim2  36796  ax12eq  36962  ax12el  36963  lshpset2N  37140  pmapglb2N  37792  pmapglb2xN  37793  pclfinN  37921  polval2N  37927  cdleme31fv2  38414  cdleme32fvcl  38461  cdleme48gfv  38558  tendoicl  38817  tendoipl  38818  diaglbN  39076  dochkr1  39499  dochkr1OLDN  39500  selvval2lem5  40236  fsuppind  40286  fsuppssind  40289  mhpind  40290  dvdsexpim  40335  nacsfix  40541  eq0rabdioph  40605  diophren  40642  rencldnfilem  40649  pell1234qrdich  40690  jm2.24  40792  jm2.26lem3  40830  wepwsolem  40874  pwssplit4  40921  isnumbasgrplem3  40937  grumnudlem  41910  cvgdvgrat  41938  ofsubid  41949  bcc0  41965  binomcxplemnn0  41974  uzwo4  42608  fiiuncl  42620  iunincfi  42651  nsstr  42652  rexanuz3  42653  iinssiin  42685  disjrnmpt2  42733  fompt  42737  disjinfi  42738  choicefi  42747  fsneq  42753  difmap  42754  iunmapsn  42764  axccdom  42769  axccd  42775  rnmptlb  42795  rnmptbd2lem  42801  ssfiunibd  42855  supxrgelem  42883  suplesup  42885  xrlexaddrp  42898  xralrple2  42900  infxrunb2  42914  xralrple3  42920  xrralrecnnle  42929  xrralrecnnge  42937  supxrunb3  42946  unb2ltle  42962  rexabslelem  42965  supminfrnmpt  42992  infxrpnf  42993  supminfxr  43011  supminfxr2  43016  xrpnf  43033  iooiinicc  43087  ressioosup  43100  iooiinioc  43101  ressiooinf  43102  fsumsupp0  43126  divcnvg  43175  limcrecl  43177  sumnnodd  43178  islpcn  43187  lptre2pt  43188  limcresiooub  43190  limcresioolb  43191  limclner  43199  fnlimfvre  43222  allbutfifvre  43223  climinf3  43264  limsupmnflem  43268  limsupre3uzlem  43283  limsupreuzmpt  43287  climuzlem  43291  climisp  43294  climrescn  43296  climxrrelem  43297  climxrre  43298  climlimsupcex  43317  liminflelimsuplem  43323  limsupgtlem  43325  liminfvalxr  43331  liminfreuzlem  43350  liminfltlem  43352  liminflimsupclim  43355  xlimpnfxnegmnf  43362  liminflbuz2  43363  liminflimsupxrre  43365  cnrefiisplem  43377  xlimmnfvlem2  43381  xlimmnfv  43382  xlimpnfvlem2  43385  xlimpnfv  43386  xlimmnfmpt  43391  xlimpnfmpt  43392  climxlim2lem  43393  dfxlim2v  43395  xlimliminflimsup  43410  cncfuni  43434  icccncfext  43435  cncficcgt0  43436  cncfiooicclem1  43441  cncfiooiccre  43443  dvasinbx  43468  dvdsn1add  43487  dvnmul  43491  dvmptfprodlem  43492  dvnprodlem1  43494  dvnprodlem3  43496  iblspltprt  43521  itgioocnicc  43525  itgspltprt  43527  ismbl3  43534  stirlinglem5  43626  dirker2re  43640  dirkerper  43644  dirkertrigeq  43649  dirkercncflem2  43652  fourierdlem12  43667  fourierdlem15  43670  fourierdlem16  43671  fourierdlem20  43675  fourierdlem21  43676  fourierdlem22  43677  fourierdlem39  43694  fourierdlem40  43695  fourierdlem41  43696  fourierdlem42  43697  fourierdlem46  43700  fourierdlem49  43703  fourierdlem50  43704  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem64  43718  fourierdlem65  43719  fourierdlem66  43720  fourierdlem68  43722  fourierdlem70  43724  fourierdlem71  43725  fourierdlem73  43727  fourierdlem78  43732  fourierdlem79  43733  fourierdlem80  43734  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem87  43741  fourierdlem93  43747  fourierdlem95  43749  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  sqwvfoura  43776  fourierswlem  43778  elaa2lem  43781  etransclem13  43795  etransclem23  43805  etransclem24  43806  etransclem32  43814  etransclem38  43820  etransclem46  43828  qndenserrnbllem  43842  rrxsnicc  43848  ioorrnopnlem  43852  prsal  43866  intsal  43876  salexct  43880  dfsalgen2  43887  issalnnd  43891  sge0rnre  43909  sge0val  43911  sge0z  43920  sge0revalmpt  43923  sge0tsms  43925  sge0pr  43939  sge0resplit  43951  sge0split  43954  sge0splitmpt  43956  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0fodjrnlem  43961  sge0iunmpt  43963  sge0rpcpnf  43966  sge0ltfirpmpt2  43971  sge0isum  43972  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0pnffsumgt  43987  sge0gtfsumgt  43988  sge0seq  43991  sge0reuz  43992  nnfoctbdjlem  44000  nnfoctbdj  44001  meadjun  44007  meadjiunlem  44010  voliunsge0lem  44017  meaiuninc3v  44029  omeiunltfirp  44064  carageniuncllem2  44067  caratheodorylem1  44071  caratheodorylem2  44072  caratheodory  44073  isomenndlem  44075  isomennd  44076  hoicvr  44093  volicorescl  44098  ovnsubaddlem2  44116  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvle  44145  ovnhoilem2  44147  hspdifhsp  44161  hoiqssbllem2  44168  hoiqssbllem3  44169  hspmbllem2  44172  ovnsubadd2lem  44190  ovolval4lem1  44194  vonvolmbl  44206  vonioo  44227  vonicc  44230  pimrecltpos  44253  issmfle  44290  smflimlem1  44316  smflimlem2  44317  smflimlem6  44321  smfresal  44333  smfrec  44334  smfmullem4  44339  smfpimcc  44352  smflimmpt  44354  smfsuplem1  44355  smfsuplem3  44357  smfsupmpt  44359  smfsupxr  44360  smfinflem  44361  smfinfmpt  44363  smflimsuplem4  44367  smflimsuplem5  44368  smflimsupmpt  44373  smfliminfmpt  44376  smonoord  44834  lswn0  44907  poprelb  44987  fmtnoprmfac1  45028  fmtnofac2lem  45031  sbgoldbst  45241  resmgmhm  45363  resmgmhm2b  45365  mgmhmco  45366  mgmhmima  45367  snlindsntorlem  45822  1arymaptf  45998  ipolubdm  46284  ipoglbdm  46287  aacllem  46516