Theorem adantll 726

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 489	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 591	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad2antlr  739  ad2ant2l  758  ad2ant2lr  760  ad5ant23  771  ad5ant24  772  ad5ant25  773  3adant1  1146  3ad2antl3  1204  ralcom2  3373  vtocl2d  3537  sbc2iegf  3827  sbcralt  3834  pofun  5585  poinxp  5740  xpdifid  6163  xpdifcnvepel  6164  sossfld  6182  preddowncl  6331  tz7.7  6384  onfr  6398  ssimaex  6964  fsneq  7028  eqfnun  7030  fndmdif  7035  dffo4  7096  fompt  7111  fcompt  7127  fconst2g  7199  f1cofveqaeq  7253  isores3  7331  limsssuc  7842  el2mpocl  8077  1stconst  8091  2ndconst  8092  curry1  8095  curry2  8098  poseq  8150  soseq  8151  extmptsuppeq  8180  suppss  8186  suppss2  8192  onnseq  8327  oe0  8503  oesuclem  8506  oecl  8518  oaordi  8527  oawordri  8531  omordi  8547  omword2  8555  omlimcl  8559  odi  8560  omass  8561  oeoe  8581  nnaordi  8600  oaabs  8630  omsmolem  8639  eceqoveq  8816  mapsnd  8880  dom2lem  8985  sbthlem9  9079  rexdif1en  9141  isinf  9221  frfi  9241  fiint  9282  fodomfib  9284  fofinf1o  9285  marypha1lem  9389  ordiso2  9473  unwdomg  9542  xpwdomg  9543  frr1  9727  ac5num  10016  cff1  10238  cfcoflem  10252  infpssrlem4  10286  isf32lem9  10341  isf34lem7  10359  fin1a2lem13  10392  fin1a2s  10394  hsmexlem4  10409  axdc2lem  10428  zorn2lem6  10481  axpowndlem2  10579  inttsk  10755  tskuni  10764  nqereu  10910  prcdnq  10974  addclprlem2  10998  ltexpri  11024  prlem936  11028  reclem2pr  11029  axsup  11281  add4  11427  ltleadd  11693  lt2mul2div  12089  nn2ge  12259  zextle  12665  fnn0ind  12691  xrlttr  13161  ifle  13219  xnn0lem1lt  13266  xaddass  13271  xmulasslem3  13308  xlemul1a  13310  xadddilem  13316  xrsupsslem  13329  xrinfmsslem  13330  supxrunb1  13341  supxrunb2  13342  ixxin  13385  difreicc  13507  iccsplit  13508  iccshftr  13509  iccshftl  13511  iccdil  13513  icccntr  13515  fzaddel  13582  fzadd2  13583  fzrev  13611  modadd1  13937  modmul1  13956  fsuppmapnn0fiub  14023  mulexp  14133  expadd  14136  expmul  14139  expnbnd  14264  bccl  14354  hashdom  14411  prsshashgt1  14443  hashfacen  14487  brfi1uzind  14541  wrdnval  14578  swrdccat3blem  14772  revccat  14799  2shfti  15113  sgn3da  15134  rexico  15401  cau3lem  15402  subcn2  15642  caucvgb  15727  iseraltlem1  15729  sumss  15771  fsumsplitsn  15791  incexclem  15886  supcvg  15906  mertenslem2  15935  fprodn0  16029  fprodsplitsn  16039  fprodle  16046  eftlcl  16159  reeftlcl  16160  rpnnen2lem6  16271  dvdsext  16375  3dvds  16385  sqoddm1div8z  16408  gcdcllem3  16555  dvdsexpim  16609  bezoutr1  16623  seq1st  16625  dvdslcm  16652  lcmeq0  16654  lcmcl  16655  lcmneg  16657  lcmdvds  16662  coprmgcdb  16703  dvdsprime  16741  pc2dvds  16935  prmpwdvds  16960  unbenlem  16964  infpnlem1  16966  1arith  16983  vdwmc2  17035  ramcl  17085  mrcuni  17673  isacs1i  17709  acsfn  17711  funcpropd  17955  curfcl  18284  curf2ndf  18299  resmgmhm  18765  resmgmhm2b  18767  mgmhmco  18768  mgmhmima  18769  resmhm  18875  resmhm2b  18877  mhmco  18878  pwsdiagmhm  18886  gsumwsubmcl  18892  gsumwspan  18901  pwmnd  18995  dfgrp2  19025  subgint  19213  ghmmhmb  19293  resghm  19298  cntzmhm  19407  symgextf1lem  19486  f1omvdconj  19512  dfod2  19630  gexdvds  19650  subgpgp  19663  sylow1lem3  19666  frgpnabllem1  19939  dprdfeq0  20090  rhmimasubrnglem  20646  cntzsubrng  20648  cntzsubr  20687  isdrng2  20823  islmodd  20961  lsslss  21056  reslmhm2b  21149  rngqiprngimfo  21408  rhmpreimaprmidl  21444  psgnfix1  21713  psgndif  21717  copsgndif  21718  ocvocv  21786  frlmsslsp  21911  frlmlbs  21912  psrbaglefi  22041  psrdi  22079  psrass23l  22081  psrass23  22083  evlsvvval  22209  rhmcomulmpl  22240  selvcllem5  22255  psdmul  22294  mptcoe1fsupp  22340  psropprmul  22362  ply1coe  22423  mamudi  22525  mamudir  22526  mat1dimelbas  22593  scmatmulcl  22640  scmatfo  22652  mulmarep1gsum2  22696  mdetunilem7  22740  mdetunilem9  22742  gsummatr01lem3  22779  smadiadetlem3  22790  cpmadugsumlemF  22998  leordtval  23335  cnpnei  23386  cnco  23388  cnss1  23398  cmpsub  23522  hauscmplem  23528  dissnlocfin  23651  ptbasid  23697  tx2cn  23732  upxp  23745  txindis  23756  xkoptsub  23776  xkopt  23777  trfbas2  23965  filconn  24005  trfil2  24009  filssufilg  24033  ufileu  24041  fixufil  24044  ufilen  24052  rnelfmlem  24074  flimclsi  24100  hauspwpwf1  24109  fclsopn  24136  fclsfnflim  24149  fclscmpi  24151  alexsubALTlem4  24172  ptcmplem5  24178  tgpmulg  24215  subgtgp  24227  tgpt0  24241  tsmsxplem2  24276  metss  24630  metustfbas  24679  dscopn  24695  xrsmopn  24935  cncfss  25023  icoopnst  25063  iccpnfcnv  25068  icccvx  25074  evth  25083  phtpycc  25115  pcohtpylem  25143  lmmbrf  25386  fgcfil  25395  caucfil  25407  cfilres  25420  bcth3  25455  cmscsscms  25497  ovolfioo  25591  ovolficc  25592  voliunlem3  25676  volcn  25730  mbflimsup  25790  mbfi1fseqlem5  25843  itg2seq  25866  bddiblnc  25966  dvnff  26047  dvnadd  26053  cpnord  26059  c1liplem1  26120  plypf1  26334  plyaddlem1  26335  plymullem1  26336  coeeulem  26346  coeidlem  26359  dgrle  26365  dgrnznn  26369  plycjlem  26398  elqaalem3  26447  ulmcaulem  26519  ulmcau  26520  psergf  26537  psercn2  26548  efopn  26785  abscxpbnd  26880  leibpi  27069  isppw2  27241  muinv  27319  bposlem3  27412  gausslemma2dlem4  27495  pntrmax  27690  pntpbnd1  27712  qabvexp  27752  madebday  28055  mulsrid  28268  bdayons  28431  peano5n0s  28474  bdaypw2n0bndlem  28618  bdayfinlem  28641  eqeelen  29191  colinearalglem4  29196  axcgrid  29203  axsegconlem1  29204  axsegconlem3  29206  ax5seglem1  29215  ax5seglem2  29216  ax5seglem9  29224  axcontlem2  29252  cusgrfilem2  29743  vtxdgfisf  29763  usgr2pthlem  30049  uspgrn2crct  30094  crctcshwlkn0  30107  wwlksnext  30179  wwlksnextproplem3  30197  eupth2lem3lem4  30519  frgr3vlem1  30561  frgr3vlem2  30562  3vfriswmgrlem  30565  frgrwopreglem5  30609  numclwwlk3lem2  30672  grpoidinvlem3  30795  grpoidinv  30797  grpoideu  30798  nmoub3i  31062  nmlno0lem  31082  nmlnoubi  31085  ipasslem3  31122  ipblnfi  31144  hvaddsub4  31367  his35  31377  shsel3  31604  chj4  31824  spansncol  31857  chscllem2  31927  5oalem2  31944  3oalem2  31952  hoaddcl  32047  adjsym  32122  cnvadj  32181  hhcno  32193  hhcnf  32194  nmopub2tALT  32198  unoplin  32209  counop  32210  nmfnleub2  32215  hmoplin  32231  brafnmul  32240  nmlnop0iALT  32284  nmopun  32303  nmophmi  32320  riesz3i  32351  riesz1  32354  cnlnadjlem2  32357  cnlnadjlem6  32361  adjmul  32381  adjadd  32382  bra11  32397  cnvbraval  32399  kbass5  32409  kbass6  32410  leop2  32413  leopadd  32421  leopmuli  32422  leoptri  32425  leopnmid  32427  nmopleid  32428  pj3si  32496  hstel2  32508  cvcon3  32573  dmdmd  32589  dmdbr5  32597  mdsl0  32599  mdslmd1lem1  32614  mdslmd1lem2  32615  mdslmd3i  32621  superpos  32643  chirredlem2  32680  chirredlem3  32681  mdsymlem3  32694  mdsymlem5  32696  mdsymlem6  32697  sumdmdlem  32707  cdjreui  32721  cdj1i  32722  cdj3i  32730  foresf1o  32787  2ndimaxp  32928  abfmpel  32937  fcomptf  32940  fcnvgreu  32954  fdifsuppconst  32971  xrge0infss  33042  xnn0gt0  33051  cycpm2tr  33376  elrgspnlem2  33500  elrgspnlem3  33501  intlidl  33668  mplvrpmga  33876  psrmonmul  33881  esplyfval0  33895  vieta  33911  lssdimle  33939  mdetpmtr1  34154  cmpcref  34181  xrge0iifcnv  34264  zrhcntr  34310  esumcst  34394  hasheuni  34416  esum2dlem  34423  esum2d  34424  sigaclcu2  34451  insiga  34468  unelldsys  34489  measres  34553  measdivcst  34555  volfiniune  34561  ddemeas  34567  actfunsnf1o  34932  fnrelpredd  35421  fineqvac  35448  fineqvnttrclselem1  35453  sconnpi1  35626  cvmsss2  35661  satfv1lem  35749  fmlaomn0  35777  gonarlem  35781  mrsubco  35908  dfon2lem6  36173  hfext  36570  elicc3  36713  fnessref  36753  bj-ismooredr2  37635  pibt2  37946  fin2solem  38140  fin2so  38141  lindsenlbs  38149  matunitlindflem1  38150  matunitlindflem2  38151  poimirlem2  38156  poimirlem14  38168  poimirlem25  38179  poimirlem26  38180  poimirlem29  38183  poimirlem30  38184  broucube  38188  heicant  38189  mblfinlem2  38192  mblfinlem3  38193  mblfinlem4  38194  ex-ovoliunnfl  38197  mbfresfi  38200  cnambfre  38202  itg2addnclem  38205  itg2addnclem2  38206  itg2addnc  38208  ftc1anclem3  38229  ftc1anclem4  38230  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  indexdom  38268  filbcmb  38274  fdc  38279  incsequz  38282  metf1o  38289  caures  38294  bndss  38320  ismtycnv  38336  heiborlem1  38345  rrncmslem  38366  isdrngo2  38492  rngoisocnv  38515  unichnidl  38565  erimeq2  39297  ax12eq  39600  ax12el  39601  lshpset2N  39778  pmapglb2N  40430  pmapglb2xN  40431  pclfinN  40559  polval2N  40565  cdleme31fv2  41052  cdleme32fvcl  41099  cdleme48gfv  41196  tendoicl  41455  tendoipl  41456  diaglbN  41714  dochkr1  42137  dochkr1OLDN  42138  sumcubes  42959  expeq1d  42970  zaddcomlem  43122  zmulcomlem  43126  fiabv  43191  rhmcomulpsr  43201  evlselv  43208  fsuppind  43209  fsuppssind  43212  mhpind  43213  nacsfix  43330  eq0rabdioph  43394  diophren  43427  rencldnfilem  43434  pell1234qrdich  43475  jm2.24  43577  jm2.26lem3  43615  wepwsolem  43656  pwssplit4  43703  isnumbasgrplem3  43719  onexoegt  43858  onov0suclim  43888  cantnfresb  43938  omcl2  43947  ofoaid1  43972  ofoaid2  43973  grumnudlem  44882  cvgdvgrat  44910  ofsubid  44921  bcc0  44937  binomcxplemnn0  44946  uzwo4  45660  fiiuncl  45672  iunincfi  45699  nsstr  45700  rexanuz3  45701  iinssiin  45734  disjrnmpt2  45793  disjinfi  45797  choicefi  45804  difmap  45810  iunmapsn  45820  axccdom  45825  axccd  45831  rnmptlb  45845  rnmptbd2lem  45850  ssfiunibd  45915  supxrgelem  45940  suplesup  45942  xrlexaddrp  45955  xralrple2  45957  infxrunb2  45970  xralrple3  45976  xrralrecnnle  45985  xrralrecnnge  45992  supxrunb3  46001  unb2ltle  46016  rexabslelem  46019  supminfrnmpt  46046  infxrpnf  46047  supminfxr  46065  supminfxr2  46070  xrpnf  46086  pimxrneun  46089  cvgcaule  46092  iooiinicc  46145  ressioosup  46158  iooiinioc  46159  ressiooinf  46160  fsumsupp0  46181  divcnvg  46230  limcrecl  46232  sumnnodd  46233  islpcn  46240  lptre2pt  46241  limcresiooub  46243  limcresioolb  46244  limclner  46252  fnlimfvre  46275  allbutfifvre  46276  climinf3  46317  limsupmnflem  46321  limsupre3uzlem  46336  limsupreuzmpt  46340  climuzlem  46344  climisp  46347  climrescn  46349  climxrrelem  46350  climxrre  46351  climlimsupcex  46370  liminflelimsuplem  46376  limsupgtlem  46378  liminfvalxr  46384  liminfreuzlem  46403  liminfltlem  46405  liminflimsupclim  46408  xlimpnfxnegmnf  46415  liminflbuz2  46416  liminflimsupxrre  46418  cnrefiisplem  46430  xlimmnfvlem2  46434  xlimmnfv  46435  xlimpnfvlem2  46438  xlimpnfv  46439  xlimmnfmpt  46444  xlimpnfmpt  46445  climxlim2lem  46446  dfxlim2v  46448  xlimliminflimsup  46463  cncfuni  46487  icccncfext  46488  cncficcgt0  46489  cncfiooicclem1  46494  cncfiooiccre  46496  dvasinbx  46521  dvdsn1add  46540  dvnmul  46544  dvmptfprodlem  46545  dvnprodlem1  46547  dvnprodlem3  46549  iblspltprt  46574  itgioocnicc  46578  itgspltprt  46580  ismbl3  46587  stirlinglem5  46679  dirker2re  46693  dirkerper  46697  dirkertrigeq  46702  dirkercncflem2  46705  fourierdlem12  46720  fourierdlem15  46723  fourierdlem16  46724  fourierdlem20  46728  fourierdlem21  46729  fourierdlem22  46730  fourierdlem39  46747  fourierdlem40  46748  fourierdlem41  46749  fourierdlem42  46750  fourierdlem46  46753  fourierdlem49  46756  fourierdlem50  46757  fourierdlem57  46764  fourierdlem58  46765  fourierdlem59  46766  fourierdlem64  46771  fourierdlem65  46772  fourierdlem66  46773  fourierdlem68  46775  fourierdlem70  46777  fourierdlem71  46778  fourierdlem73  46780  fourierdlem78  46785  fourierdlem79  46786  fourierdlem80  46787  fourierdlem81  46788  fourierdlem82  46789  fourierdlem83  46790  fourierdlem87  46794  fourierdlem93  46800  fourierdlem95  46802  fourierdlem101  46808  fourierdlem103  46810  fourierdlem104  46811  fourierdlem111  46818  fourierdlem112  46819  sqwvfoura  46829  fourierswlem  46831  elaa2lem  46834  etransclem13  46848  etransclem23  46858  etransclem24  46859  etransclem32  46867  etransclem38  46873  etransclem46  46881  qndenserrnbllem  46895  rrxsnicc  46901  ioorrnopnlem  46905  prsal  46919  intsal  46931  salexct  46935  dfsalgen2  46942  issalnnd  46946  sge0rnre  46965  sge0val  46967  sge0z  46976  sge0revalmpt  46979  sge0tsms  46981  sge0pr  46995  sge0resplit  47007  sge0split  47010  sge0splitmpt  47012  sge0iunmptlemfi  47014  sge0iunmptlemre  47016  sge0fodjrnlem  47017  sge0iunmpt  47019  sge0rpcpnf  47022  sge0ltfirpmpt2  47027  sge0isum  47028  sge0xaddlem1  47034  sge0xaddlem2  47035  sge0pnffsumgt  47043  sge0gtfsumgt  47044  sge0seq  47047  sge0reuz  47048  nnfoctbdjlem  47056  nnfoctbdj  47057  meadjun  47063  meadjiunlem  47066  voliunsge0lem  47073  meaiuninc3v  47085  omeiunltfirp  47120  carageniuncllem2  47123  caratheodorylem1  47127  caratheodorylem2  47128  caratheodory  47129  isomenndlem  47131  isomennd  47132  hoicvr  47149  volicorescl  47154  ovnsubaddlem2  47172  hoidmvlelem2  47197  hoidmvlelem3  47198  hoidmvle  47201  ovnhoilem2  47203  hspdifhsp  47217  hoiqssbllem2  47224  hoiqssbllem3  47225  hspmbllem2  47228  ovnsubadd2lem  47246  ovolval4lem1  47250  vonvolmbl  47262  vonioo  47283  vonicc  47286  pimrecltpos  47309  issmfle  47346  smflimlem1  47372  smflimlem2  47373  smflimlem6  47377  smfresal  47389  smfrec  47390  smfmullem4  47395  smfpimcc  47409  smflimmpt  47411  smfsuplem1  47412  smfsuplem3  47414  smfsupmpt  47416  smfsupxr  47417  smfinflem  47418  smfinfmpt  47420  smflimsuplem4  47424  smflimsuplem5  47425  smflimsupmpt  47430  smfliminfmpt  47433  fsupdm  47443  finfdm  47447  smonoord  47998  lswn0  48077  poprelb  48157  fmtnoprmfac1  48201  fmtnofac2lem  48204  sbgoldbst  48427  isgrim  48531  gpgedgvtx0  48710  snlindsntorlem  49130  1arymaptf  49301  ipolubdm  49645  ipoglbdm  49648  setc1onsubc  50260  aacllem  50470