Theorem adantll 720

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 586	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 208  df-an 397

This theorem is referenced by:  ad2antlr  733  ad2ant2l  752  ad2ant2lr  754  ad5ant23  765  ad5ant24  766  ad5ant25  767  3adant1  1136  3ad2antl3  1194  ralcom2  3341  vtocl2d  3507  sbc2iegf  3797  sbcralt  3804  pofun  5544  poinxp  5699  xpdifid  6119  sossfld  6137  preddowncl  6283  tz7.7  6336  onfr  6349  ssimaex  6912  fsneq  6976  eqfnun  6978  fndmdif  6983  dffo4  7044  fompt  7059  fcompt  7075  fconst2g  7147  f1cofveqaeq  7201  isores3  7279  limsssuc  7790  el2mpocl  8025  1stconst  8039  2ndconst  8040  curry1  8043  curry2  8046  poseq  8098  soseq  8099  extmptsuppeq  8128  suppss  8134  suppss2  8140  onnseq  8274  oe0  8447  oesuclem  8450  oecl  8462  oaordi  8471  oawordri  8475  omordi  8491  omword2  8499  omlimcl  8503  odi  8504  omass  8505  oeoe  8525  nnaordi  8544  oaabs  8574  omsmolem  8583  eceqoveq  8759  mapsnd  8824  dom2lem  8929  sbthlem9  9023  rexdif1en  9085  isinf  9165  frfi  9185  fiint  9227  fodomfib  9229  fodomfibOLD  9231  fofinf1o  9232  marypha1lem  9336  ordiso2  9420  unwdomg  9489  xpwdomg  9490  frr1  9674  ac5num  9949  cff1  10171  cfcoflem  10185  infpssrlem4  10219  isf32lem9  10274  isf34lem7  10292  fin1a2lem13  10325  fin1a2s  10327  hsmexlem4  10342  axdc2lem  10361  zorn2lem6  10414  axpowndlem2  10512  inttsk  10688  tskuni  10697  nqereu  10843  prcdnq  10907  addclprlem2  10931  ltexpri  10957  prlem936  10961  reclem2pr  10962  axsup  11212  add4  11358  ltleadd  11624  lt2mul2div  12025  nn2ge  12195  zextle  12593  fnn0ind  12619  xrlttr  13082  ifle  13140  xnn0lem1lt  13187  xaddass  13192  xmulasslem3  13229  xlemul1a  13231  xadddilem  13237  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  ixxin  13306  difreicc  13428  iccsplit  13429  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  fzaddel  13503  fzadd2  13504  fzrev  13532  modadd1  13858  modmul1  13877  fsuppmapnn0fiub  13944  mulexp  14054  expadd  14057  expmul  14060  expnbnd  14185  bccl  14275  hashdom  14332  prsshashgt1  14363  hashfacen  14407  brfi1uzind  14461  wrdnval  14498  swrdccat3blem  14692  revccat  14719  2shfti  15033  rexico  15307  cau3lem  15308  subcn2  15548  caucvgb  15633  iseraltlem1  15635  sumss  15677  fsumsplitsn  15697  incexclem  15792  supcvg  15812  mertenslem2  15841  fprodn0  15935  fprodsplitsn  15945  fprodle  15952  eftlcl  16065  reeftlcl  16066  rpnnen2lem6  16177  dvdsext  16281  3dvds  16291  sqoddm1div8z  16314  gcdcllem3  16461  dvdsexpim  16515  bezoutr1  16529  seq1st  16531  dvdslcm  16558  lcmeq0  16560  lcmcl  16561  lcmneg  16563  lcmdvds  16568  coprmgcdb  16609  dvdsprime  16647  pc2dvds  16841  prmpwdvds  16866  unbenlem  16870  infpnlem1  16872  1arith  16889  vdwmc2  16941  ramcl  16991  mrcuni  17578  isacs1i  17614  acsfn  17616  funcpropd  17860  curfcl  18189  curf2ndf  18204  resmgmhm  18670  resmgmhm2b  18672  mgmhmco  18673  mgmhmima  18674  resmhm  18779  resmhm2b  18781  mhmco  18782  pwsdiagmhm  18790  gsumwsubmcl  18796  gsumwspan  18805  pwmnd  18899  dfgrp2  18929  subgint  19117  ghmmhmb  19193  resghm  19198  cntzmhm  19307  symgextf1lem  19386  f1omvdconj  19412  dfod2  19530  gexdvds  19550  subgpgp  19563  sylow1lem3  19566  frgpnabllem1  19839  dprdfeq0  19990  rhmimasubrnglem  20537  cntzsubrng  20539  cntzsubr  20578  isdrng2  20715  islmodd  20856  lsslss  20951  reslmhm2b  21044  rngqiprngimfo  21294  psgnfix1  21573  psgndif  21577  copsgndif  21578  ocvocv  21646  frlmsslsp  21771  frlmlbs  21772  psrbaglefi  21901  psrdi  21939  psrass23l  21941  psrass23  21943  evlsvvval  22069  rhmcomulmpl  22100  selvcllem5  22115  psdmul  22154  mptcoe1fsupp  22200  psropprmul  22222  ply1coe  22284  mamudi  22386  mamudir  22387  mat1dimelbas  22454  scmatmulcl  22501  scmatfo  22513  mulmarep1gsum2  22557  mdetunilem7  22601  mdetunilem9  22603  gsummatr01lem3  22640  smadiadetlem3  22651  cpmadugsumlemF  22859  leordtval  23196  cnpnei  23247  cnco  23249  cnss1  23259  cmpsub  23383  hauscmplem  23389  dissnlocfin  23512  ptbasid  23558  tx2cn  23593  upxp  23606  txindis  23617  xkoptsub  23637  xkopt  23638  trfbas2  23826  filconn  23866  trfil2  23870  filssufilg  23894  ufileu  23902  fixufil  23905  ufilen  23913  rnelfmlem  23935  flimclsi  23961  hauspwpwf1  23970  fclsopn  23997  fclsfnflim  24010  fclscmpi  24012  alexsubALTlem4  24033  ptcmplem5  24039  tgpmulg  24076  subgtgp  24088  tgpt0  24102  tsmsxplem2  24137  metss  24491  metustfbas  24540  dscopn  24556  xrsmopn  24796  cncfss  24884  icoopnst  24924  iccpnfcnv  24929  icccvx  24935  evth  24944  phtpycc  24976  pcohtpylem  25004  lmmbrf  25247  fgcfil  25256  caucfil  25268  cfilres  25281  bcth3  25316  cmscsscms  25358  ovolfioo  25452  ovolficc  25453  voliunlem3  25537  volcn  25591  mbflimsup  25651  mbfi1fseqlem5  25704  itg2seq  25727  bddiblnc  25827  dvnff  25908  dvnadd  25914  cpnord  25920  c1liplem1  25981  plypf1  26195  plyaddlem1  26196  plymullem1  26197  coeeulem  26207  coeidlem  26220  dgrle  26226  dgrnznn  26230  plycjlem  26259  elqaalem3  26305  ulmcaulem  26377  ulmcau  26378  psergf  26395  psercn2  26406  efopn  26640  abscxpbnd  26735  leibpi  26924  isppw2  27096  muinv  27174  bposlem3  27267  gausslemma2dlem4  27350  pntrmax  27545  pntpbnd1  27567  qabvexp  27607  madebday  27910  mulsrid  28123  bdayons  28286  peano5n0s  28329  bdaypw2n0bndlem  28473  bdayfinlem  28496  eqeelen  28991  colinearalglem4  28996  axcgrid  29003  axsegconlem1  29004  axsegconlem3  29006  ax5seglem1  29015  ax5seglem2  29016  ax5seglem9  29024  axcontlem2  29052  cusgrfilem2  29543  vtxdgfisf  29563  usgr2pthlem  29849  uspgrn2crct  29894  crctcshwlkn0  29907  wwlksnext  29979  wwlksnextproplem3  29997  eupth2lem3lem4  30319  frgr3vlem1  30361  frgr3vlem2  30362  3vfriswmgrlem  30365  frgrwopreglem5  30409  numclwwlk3lem2  30472  grpoidinvlem3  30595  grpoidinv  30597  grpoideu  30598  nmoub3i  30862  nmlno0lem  30882  nmlnoubi  30885  ipasslem3  30922  ipblnfi  30944  hvaddsub4  31167  his35  31177  shsel3  31404  chj4  31624  spansncol  31657  chscllem2  31727  5oalem2  31744  3oalem2  31752  hoaddcl  31847  adjsym  31922  cnvadj  31981  hhcno  31993  hhcnf  31994  nmopub2tALT  31998  unoplin  32009  counop  32010  nmfnleub2  32015  hmoplin  32031  brafnmul  32040  nmlnop0iALT  32084  nmopun  32103  nmophmi  32120  riesz3i  32151  riesz1  32154  cnlnadjlem2  32157  cnlnadjlem6  32161  adjmul  32181  adjadd  32182  bra11  32197  cnvbraval  32199  kbass5  32209  kbass6  32210  leop2  32213  leopadd  32221  leopmuli  32222  leoptri  32225  leopnmid  32227  nmopleid  32228  pj3si  32296  hstel2  32308  cvcon3  32373  dmdmd  32389  dmdbr5  32397  mdsl0  32399  mdslmd1lem1  32414  mdslmd1lem2  32415  mdslmd3i  32421  superpos  32443  chirredlem2  32480  chirredlem3  32481  mdsymlem3  32494  mdsymlem5  32496  mdsymlem6  32497  sumdmdlem  32507  cdjreui  32521  cdj1i  32522  cdj3i  32530  foresf1o  32592  2ndimaxp  32738  abfmpel  32747  fcomptf  32750  fcnvgreu  32764  fdifsuppconst  32781  xrge0infss  32852  xnn0gt0  32861  sgn3da  32926  cycpm2tr  33200  elrgspnlem2  33324  elrgspnlem3  33325  intlidl  33503  rhmpreimaprmidl  33534  mplvrpmga  33729  psrmonmul  33734  esplyfval0  33748  vieta  33764  lssdimle  33792  mdetpmtr1  34007  cmpcref  34034  xrge0iifcnv  34117  zrhcntr  34163  esumcst  34247  hasheuni  34269  esum2dlem  34276  esum2d  34277  sigaclcu2  34304  insiga  34321  unelldsys  34342  measres  34406  measdivcst  34408  volfiniune  34414  ddemeas  34420  actfunsnf1o  34788  fnrelpredd  35272  fineqvac  35297  fineqvnttrclselem1  35302  sconnpi1  35467  cvmsss2  35502  satfv1lem  35590  fmlaomn0  35618  gonarlem  35622  mrsubco  35749  dfon2lem6  36014  hfext  36411  elicc3  36545  fnessref  36585  bj-ismooredr2  37468  pibt2  37779  fin2solem  37973  fin2so  37974  lindsenlbs  37982  matunitlindflem1  37983  matunitlindflem2  37984  poimirlem2  37989  poimirlem14  38001  poimirlem25  38012  poimirlem26  38013  poimirlem29  38016  poimirlem30  38017  broucube  38021  heicant  38022  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  ex-ovoliunnfl  38030  mbfresfi  38033  cnambfre  38035  itg2addnclem  38038  itg2addnclem2  38039  itg2addnc  38041  ftc1anclem3  38062  ftc1anclem4  38063  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  indexdom  38101  filbcmb  38107  fdc  38112  incsequz  38115  metf1o  38122  caures  38127  bndss  38153  ismtycnv  38169  heiborlem1  38178  rrncmslem  38199  isdrngo2  38325  rngoisocnv  38348  unichnidl  38398  erimeq2  39130  ax12eq  39433  ax12el  39434  lshpset2N  39611  pmapglb2N  40263  pmapglb2xN  40264  pclfinN  40392  polval2N  40398  cdleme31fv2  40885  cdleme32fvcl  40932  cdleme48gfv  41029  tendoicl  41288  tendoipl  41289  diaglbN  41547  dochkr1  41970  dochkr1OLDN  41971  sumcubes  42790  expeq1d  42801  zaddcomlem  42953  zmulcomlem  42957  fiabv  43022  rhmcomulpsr  43032  evlselv  43039  fsuppind  43040  fsuppssind  43043  mhpind  43044  nacsfix  43161  eq0rabdioph  43225  diophren  43258  rencldnfilem  43265  pell1234qrdich  43306  jm2.24  43408  jm2.26lem3  43446  wepwsolem  43487  pwssplit4  43534  isnumbasgrplem3  43550  onexoegt  43689  onov0suclim  43719  cantnfresb  43769  omcl2  43778  ofoaid1  43803  ofoaid2  43804  grumnudlem  44729  cvgdvgrat  44757  ofsubid  44768  bcc0  44784  binomcxplemnn0  44793  uzwo4  45501  fiiuncl  45513  iunincfi  45541  nsstr  45542  rexanuz3  45543  iinssiin  45576  disjrnmpt2  45635  disjinfi  45639  choicefi  45646  difmap  45652  iunmapsn  45662  axccdom  45667  axccd  45673  rnmptlb  45687  rnmptbd2lem  45692  ssfiunibd  45757  supxrgelem  45782  suplesup  45784  xrlexaddrp  45797  xralrple2  45799  infxrunb2  45812  xralrple3  45818  xrralrecnnle  45827  xrralrecnnge  45834  supxrunb3  45843  unb2ltle  45858  rexabslelem  45861  supminfrnmpt  45888  infxrpnf  45889  supminfxr  45907  supminfxr2  45912  xrpnf  45928  pimxrneun  45931  cvgcaule  45934  iooiinicc  45987  ressioosup  46000  iooiinioc  46001  ressiooinf  46002  fsumsupp0  46023  divcnvg  46072  limcrecl  46074  sumnnodd  46075  islpcn  46082  lptre2pt  46083  limcresiooub  46085  limcresioolb  46086  limclner  46094  fnlimfvre  46117  allbutfifvre  46118  climinf3  46159  limsupmnflem  46163  limsupre3uzlem  46178  limsupreuzmpt  46182  climuzlem  46186  climisp  46189  climrescn  46191  climxrrelem  46192  climxrre  46193  climlimsupcex  46212  liminflelimsuplem  46218  limsupgtlem  46220  liminfvalxr  46226  liminfreuzlem  46245  liminfltlem  46247  liminflimsupclim  46250  xlimpnfxnegmnf  46257  liminflbuz2  46258  liminflimsupxrre  46260  cnrefiisplem  46272  xlimmnfvlem2  46276  xlimmnfv  46277  xlimpnfvlem2  46280  xlimpnfv  46281  xlimmnfmpt  46286  xlimpnfmpt  46287  climxlim2lem  46288  dfxlim2v  46290  xlimliminflimsup  46305  cncfuni  46329  icccncfext  46330  cncficcgt0  46331  cncfiooicclem1  46336  cncfiooiccre  46338  dvasinbx  46363  dvdsn1add  46382  dvnmul  46386  dvmptfprodlem  46387  dvnprodlem1  46389  dvnprodlem3  46391  iblspltprt  46416  itgioocnicc  46420  itgspltprt  46422  ismbl3  46429  stirlinglem5  46521  dirker2re  46535  dirkerper  46539  dirkertrigeq  46544  dirkercncflem2  46547  fourierdlem12  46562  fourierdlem15  46565  fourierdlem16  46566  fourierdlem20  46570  fourierdlem21  46571  fourierdlem22  46572  fourierdlem39  46589  fourierdlem40  46590  fourierdlem41  46591  fourierdlem42  46592  fourierdlem46  46595  fourierdlem49  46598  fourierdlem50  46599  fourierdlem57  46606  fourierdlem58  46607  fourierdlem59  46608  fourierdlem64  46613  fourierdlem65  46614  fourierdlem66  46615  fourierdlem68  46617  fourierdlem70  46619  fourierdlem71  46620  fourierdlem73  46622  fourierdlem78  46627  fourierdlem79  46628  fourierdlem80  46629  fourierdlem81  46630  fourierdlem82  46631  fourierdlem83  46632  fourierdlem87  46636  fourierdlem93  46642  fourierdlem95  46644  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  sqwvfoura  46671  fourierswlem  46673  elaa2lem  46676  etransclem13  46690  etransclem23  46700  etransclem24  46701  etransclem32  46709  etransclem38  46715  etransclem46  46723  qndenserrnbllem  46737  rrxsnicc  46743  ioorrnopnlem  46747  prsal  46761  intsal  46773  salexct  46777  dfsalgen2  46784  issalnnd  46788  sge0rnre  46807  sge0val  46809  sge0z  46818  sge0revalmpt  46821  sge0tsms  46823  sge0pr  46837  sge0resplit  46849  sge0split  46852  sge0splitmpt  46854  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0fodjrnlem  46859  sge0iunmpt  46861  sge0rpcpnf  46864  sge0ltfirpmpt2  46869  sge0isum  46870  sge0xaddlem1  46876  sge0xaddlem2  46877  sge0pnffsumgt  46885  sge0gtfsumgt  46886  sge0seq  46889  sge0reuz  46890  nnfoctbdjlem  46898  nnfoctbdj  46899  meadjun  46905  meadjiunlem  46908  voliunsge0lem  46915  meaiuninc3v  46927  omeiunltfirp  46962  carageniuncllem2  46965  caratheodorylem1  46969  caratheodorylem2  46970  caratheodory  46971  isomenndlem  46973  isomennd  46974  hoicvr  46991  volicorescl  46996  ovnsubaddlem2  47014  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvle  47043  ovnhoilem2  47045  hspdifhsp  47059  hoiqssbllem2  47066  hoiqssbllem3  47067  hspmbllem2  47070  ovnsubadd2lem  47088  ovolval4lem1  47092  vonvolmbl  47104  vonioo  47125  vonicc  47128  pimrecltpos  47151  issmfle  47188  smflimlem1  47214  smflimlem2  47215  smflimlem6  47219  smfresal  47231  smfrec  47232  smfmullem4  47237  smfpimcc  47251  smflimmpt  47253  smfsuplem1  47254  smfsuplem3  47256  smfsupmpt  47258  smfsupxr  47259  smfinflem  47260  smfinfmpt  47262  smflimsuplem4  47266  smflimsuplem5  47267  smflimsupmpt  47272  smfliminfmpt  47275  fsupdm  47285  finfdm  47289  smonoord  47840  lswn0  47919  poprelb  47999  fmtnoprmfac1  48043  fmtnofac2lem  48046  sbgoldbst  48269  isgrim  48373  gpgedgvtx0  48552  snlindsntorlem  48961  1arymaptf  49132  ipolubdm  49477  ipoglbdm  49480  setc1onsubc  50092  aacllem  50291