Theorem adantll 712

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  725  ad2ant2l  744  ad2ant2lr  746  ad5ant23  758  ad5ant24  759  ad5ant25  760  3adant1  1130  3ad2antl3  1187  ralcom2  3372  vtocl2d  3541  sbc2iegf  3855  sbcralt  3862  pofun  5599  poinxp  5748  xpdifid  6156  sossfld  6174  preddowncl  6322  tz7.7  6379  onfr  6392  ssimaex  6962  fndmdif  7028  dffo4  7089  fcompt  7115  fconst2g  7188  f1cofveqaeq  7241  2f1fvneq  7243  isores3  7316  fvmptopabOLD  7448  limsssuc  7822  el2mpocl  8054  1stconst  8068  2ndconst  8069  curry1  8072  curry2  8075  poseq  8126  soseq  8127  extmptsuppeq  8155  suppss  8161  suppssOLD  8162  suppssov1  8165  suppss2  8167  onnseq  8326  oe0  8504  oesuclem  8507  oecl  8519  oaordi  8529  oawordri  8533  omordi  8549  omword2  8557  omlimcl  8561  odi  8562  omass  8563  oeoe  8582  nnaordi  8601  oaabs  8630  omsmolem  8639  eceqoveq  8799  mapsnd  8863  dom2lem  8971  sbthlem9  9074  rexdif1en  9141  php3OLD  9207  onomeneqOLD  9212  isinf  9243  isinfOLD  9244  frfi  9271  fiint  9307  fodomfib  9309  fofinf1o  9310  marypha1lem  9410  ordiso2  9492  unwdomg  9561  xpwdomg  9562  frr1  9736  ac5num  10013  cff1  10235  cfcoflem  10249  infpssrlem4  10283  isf32lem9  10338  isf34lem7  10356  fin1a2lem13  10389  fin1a2s  10391  hsmexlem4  10406  axdc2lem  10425  zorn2lem6  10478  axpowndlem2  10575  inttsk  10751  tskuni  10760  nqereu  10906  prcdnq  10970  addclprlem2  10994  ltexpri  11020  prlem936  11024  reclem2pr  11025  axsup  11271  add4  11416  ltleadd  11679  lt2mul2div  12074  nn2ge  12221  zextle  12617  fnn0ind  12643  xrlttr  13101  ifle  13158  xnn0lem1lt  13205  xaddass  13210  xmulasslem3  13247  xlemul1a  13249  xadddilem  13255  xrsupsslem  13268  xrinfmsslem  13269  supxrunb1  13280  supxrunb2  13281  ixxin  13323  difreicc  13443  iccsplit  13444  iccshftr  13445  iccshftl  13447  iccdil  13449  icccntr  13451  fzaddel  13517  fzadd2  13518  fzrev  13546  modadd1  13855  modmul1  13871  fsuppmapnn0fiub  13938  mulexp  14049  expadd  14052  expmul  14055  expnbnd  14177  bccl  14264  hashdom  14321  prsshashgt1  14352  hashfacen  14395  hashfacenOLD  14396  brfi1uzind  14441  wrdnval  14477  swrdccat3blem  14671  revccat  14698  2shfti  15009  rexico  15282  cau3lem  15283  subcn2  15521  caucvgb  15608  iseraltlem1  15610  sumss  15652  fsumsplitsn  15672  incexclem  15764  supcvg  15784  mertenslem2  15813  fprodn0  15905  fprodsplitsn  15915  fprodle  15922  eftlcl  16032  reeftlcl  16033  rpnnen2lem6  16144  dvdsext  16246  3dvds  16256  sqoddm1div8z  16279  gcdcllem3  16424  bezoutr1  16488  seq1st  16490  dvdslcm  16517  lcmeq0  16519  lcmcl  16520  lcmneg  16522  lcmdvds  16527  coprmgcdb  16568  dvdsprime  16606  pc2dvds  16794  prmpwdvds  16819  unbenlem  16823  infpnlem1  16825  1arith  16842  vdwmc2  16894  ramcl  16944  mrcuni  17547  isacs1i  17583  acsfn  17585  funcpropd  17833  curfcl  18167  curf2ndf  18182  resmhm  18677  resmhm2b  18679  mhmco  18680  mhmima  18681  pwsdiagmhm  18687  gsumwsubmcl  18693  gsumwspan  18702  pwmnd  18793  dfgrp2  18822  subgint  19002  ghmmhmb  19069  resghm  19074  cntzmhm  19169  symgextf1lem  19252  f1omvdconj  19278  dfod2  19396  gexdvds  19416  subgpgp  19429  sylow1lem3  19432  frgpnabllem1  19701  dprdfeq0  19851  isdrng2  20278  cntzsubr  20347  islmodd  20426  lsslss  20521  reslmhm2b  20614  psgnfix1  21084  psgndif  21088  copsgndif  21089  ocvocv  21157  frlmsslsp  21284  frlmlbs  21285  psrbaglefi  21416  psrbaglefiOLD  21417  mptcoe1fsupp  21668  psropprmul  21691  ply1coe  21749  mamudi  21832  mamudir  21833  mat1dimelbas  21902  scmatmulcl  21949  scmatfo  21961  mulmarep1gsum2  22005  mdetunilem7  22049  mdetunilem9  22051  gsummatr01lem3  22088  smadiadetlem3  22099  cpmadugsumlemF  22307  leordtval  22646  cnpnei  22697  cnco  22699  cnss1  22709  cmpsub  22833  hauscmplem  22839  dissnlocfin  22962  ptbasid  23008  tx2cn  23043  upxp  23056  txindis  23067  xkoptsub  23087  xkopt  23088  trfbas2  23276  filconn  23316  trfil2  23320  filssufilg  23344  ufileu  23352  fixufil  23355  ufilen  23363  rnelfmlem  23385  flimclsi  23411  hauspwpwf1  23420  fclsopn  23447  fclsfnflim  23460  fclscmpi  23462  alexsubALTlem4  23483  ptcmplem5  23489  tgpmulg  23526  subgtgp  23538  tgpt0  23552  tsmsxplem2  23587  metss  23946  metustfbas  23995  dscopn  24011  xrsmopn  24257  cncfss  24344  icoopnst  24384  iccpnfcnv  24389  icccvx  24395  evth  24404  phtpycc  24436  pcohtpylem  24464  lmmbrf  24708  fgcfil  24717  caucfil  24729  cfilres  24742  bcth3  24777  cmscsscms  24819  ovolfioo  24913  ovolficc  24914  voliunlem3  24998  volcn  25052  mbflimsup  25112  mbfi1fseqlem5  25166  itg2seq  25189  bddiblnc  25288  dvnff  25369  dvnadd  25375  cpnord  25381  c1liplem1  25442  plypf1  25655  plyaddlem1  25656  plymullem1  25657  coeeulem  25667  coeidlem  25680  dgrle  25686  dgrnznn  25690  plycjlem  25719  elqaalem3  25763  ulmcaulem  25835  ulmcau  25836  psergf  25853  psercn2  25864  efopn  26095  abscxpbnd  26188  leibpi  26374  isppw2  26546  muinv  26624  bposlem3  26716  gausslemma2dlem4  26799  pntrmax  26994  pntpbnd1  27016  qabvexp  27056  madebday  27317  mulsrid  27483  eqeelen  28027  colinearalglem4  28032  axcgrid  28039  axsegconlem1  28040  axsegconlem3  28042  ax5seglem1  28051  ax5seglem2  28052  ax5seglem9  28060  axcontlem2  28088  cusgrfilem2  28578  vtxdgfisf  28598  usgr2pthlem  28885  uspgrn2crct  28927  crctcshwlkn0  28940  wwlksnext  29012  wwlksnextproplem3  29030  eupth2lem3lem4  29349  frgr3vlem1  29391  frgr3vlem2  29392  3vfriswmgrlem  29395  frgrwopreglem5  29439  numclwwlk3lem2  29502  grpoidinvlem3  29622  grpoidinv  29624  grpoideu  29625  nmoub3i  29889  nmlno0lem  29909  nmlnoubi  29912  ipasslem3  29949  ipblnfi  29971  hvaddsub4  30194  his35  30204  shsel3  30431  chj4  30651  spansncol  30684  chscllem2  30754  5oalem2  30771  3oalem2  30779  hoaddcl  30874  adjsym  30949  cnvadj  31008  hhcno  31020  hhcnf  31021  nmopub2tALT  31025  unoplin  31036  counop  31037  nmfnleub2  31042  hmoplin  31058  brafnmul  31067  nmlnop0iALT  31111  nmopun  31130  nmophmi  31147  riesz3i  31178  riesz1  31181  cnlnadjlem2  31184  cnlnadjlem6  31188  adjmul  31208  adjadd  31209  bra11  31224  cnvbraval  31226  kbass5  31236  kbass6  31237  leop2  31240  leopadd  31248  leopmuli  31249  leoptri  31252  leopnmid  31254  nmopleid  31255  pj3si  31323  hstel2  31335  cvcon3  31400  dmdmd  31416  dmdbr5  31424  mdsl0  31426  mdslmd1lem1  31441  mdslmd1lem2  31442  mdslmd3i  31448  superpos  31470  chirredlem2  31507  chirredlem3  31508  mdsymlem3  31521  mdsymlem5  31523  mdsymlem6  31524  sumdmdlem  31534  cdjreui  31548  cdj1i  31549  cdj3i  31557  foresf1o  31606  2ndimaxp  31741  abfmpel  31749  fcomptf  31752  fcnvgreu  31767  fdifsuppconst  31782  xrge0infss  31844  xnn0gt0  31853  cycpm2tr  32149  intlidl  32391  rhmpreimaprmidl  32421  lssdimle  32531  mdetpmtr1  32634  cmpcref  32661  xrge0iifcnv  32744  esumcst  32892  hasheuni  32914  esum2dlem  32921  esum2d  32922  sigaclcu2  32949  insiga  32966  unelldsys  32987  measres  33051  measdivcst  33053  volfiniune  33059  ddemeas  33065  sgn3da  33371  actfunsnf1o  33447  fnrelpredd  33923  fineqvac  33928  sconnpi1  34061  cvmsss2  34096  satfv1lem  34184  fmlaomn0  34212  gonarlem  34216  mrsubco  34343  dfon2lem6  34590  hfext  34985  elicc3  35006  fnessref  35046  bj-ismooredr2  35795  pibt2  36102  fin2solem  36278  fin2so  36279  lindsenlbs  36287  matunitlindflem1  36288  matunitlindflem2  36289  poimirlem2  36294  poimirlem14  36306  poimirlem25  36317  poimirlem26  36318  poimirlem29  36321  poimirlem30  36322  broucube  36326  heicant  36327  mblfinlem2  36330  mblfinlem3  36331  mblfinlem4  36332  ex-ovoliunnfl  36335  mbfresfi  36338  cnambfre  36340  itg2addnclem  36343  itg2addnclem2  36344  itg2addnc  36346  ftc1anclem3  36367  ftc1anclem4  36368  ftc1anclem5  36369  ftc1anclem6  36370  ftc1anclem7  36371  ftc1anclem8  36372  ftc1anc  36373  eqfnun  36395  indexdom  36407  filbcmb  36413  fdc  36418  incsequz  36421  metf1o  36428  caures  36433  bndss  36459  ismtycnv  36475  heiborlem1  36484  rrncmslem  36505  isdrngo2  36631  rngoisocnv  36654  unichnidl  36704  erimeq2  37353  ax12eq  37616  ax12el  37617  lshpset2N  37794  pmapglb2N  38447  pmapglb2xN  38448  pclfinN  38576  polval2N  38582  cdleme31fv2  39069  cdleme32fvcl  39116  cdleme48gfv  39213  tendoicl  39472  tendoipl  39473  diaglbN  39731  dochkr1  40154  dochkr1OLDN  40155  selvcllem5  40946  fsuppind  40951  fsuppssind  40954  mhpind  40955  dvdsexpim  41000  zaddcomlem  41106  zmulcomlem  41110  nacsfix  41221  eq0rabdioph  41285  diophren  41322  rencldnfilem  41329  pell1234qrdich  41370  jm2.24  41473  jm2.26lem3  41511  wepwsolem  41555  pwssplit4  41602  isnumbasgrplem3  41618  onexoegt  41764  onov0suclim  41795  cantnfresb  41845  omcl2  41854  ofoaid1  41879  ofoaid2  41880  grumnudlem  42815  cvgdvgrat  42843  ofsubid  42854  bcc0  42870  binomcxplemnn0  42879  uzwo4  43511  fiiuncl  43523  iunincfi  43554  nsstr  43555  rexanuz3  43556  iinssiin  43589  disjrnmpt2  43657  fompt  43661  disjinfi  43662  choicefi  43670  fsneq  43676  difmap  43677  iunmapsn  43687  axccdom  43692  axccd  43699  rnmptlb  43719  rnmptbd2lem  43725  ssfiunibd  43792  supxrgelem  43820  suplesup  43822  xrlexaddrp  43835  xralrple2  43837  infxrunb2  43851  xralrple3  43857  xrralrecnnle  43866  xrralrecnnge  43873  supxrunb3  43882  unb2ltle  43898  rexabslelem  43901  supminfrnmpt  43928  infxrpnf  43929  supminfxr  43947  supminfxr2  43952  xrpnf  43969  pimxrneun  43972  cvgcaule  43975  iooiinicc  44028  ressioosup  44041  iooiinioc  44042  ressiooinf  44043  fsumsupp0  44067  divcnvg  44116  limcrecl  44118  sumnnodd  44119  islpcn  44128  lptre2pt  44129  limcresiooub  44131  limcresioolb  44132  limclner  44140  fnlimfvre  44163  allbutfifvre  44164  climinf3  44205  limsupmnflem  44209  limsupre3uzlem  44224  limsupreuzmpt  44228  climuzlem  44232  climisp  44235  climrescn  44237  climxrrelem  44238  climxrre  44239  climlimsupcex  44258  liminflelimsuplem  44264  limsupgtlem  44266  liminfvalxr  44272  liminfreuzlem  44291  liminfltlem  44293  liminflimsupclim  44296  xlimpnfxnegmnf  44303  liminflbuz2  44304  liminflimsupxrre  44306  cnrefiisplem  44318  xlimmnfvlem2  44322  xlimmnfv  44323  xlimpnfvlem2  44326  xlimpnfv  44327  xlimmnfmpt  44332  xlimpnfmpt  44333  climxlim2lem  44334  dfxlim2v  44336  xlimliminflimsup  44351  cncfuni  44375  icccncfext  44376  cncficcgt0  44377  cncfiooicclem1  44382  cncfiooiccre  44384  dvasinbx  44409  dvdsn1add  44428  dvnmul  44432  dvmptfprodlem  44433  dvnprodlem1  44435  dvnprodlem3  44437  iblspltprt  44462  itgioocnicc  44466  itgspltprt  44468  ismbl3  44475  stirlinglem5  44567  dirker2re  44581  dirkerper  44585  dirkertrigeq  44590  dirkercncflem2  44593  fourierdlem12  44608  fourierdlem15  44611  fourierdlem16  44612  fourierdlem20  44616  fourierdlem21  44617  fourierdlem22  44618  fourierdlem39  44635  fourierdlem40  44636  fourierdlem41  44637  fourierdlem42  44638  fourierdlem46  44641  fourierdlem49  44644  fourierdlem50  44645  fourierdlem57  44652  fourierdlem58  44653  fourierdlem59  44654  fourierdlem64  44659  fourierdlem65  44660  fourierdlem66  44661  fourierdlem68  44663  fourierdlem70  44665  fourierdlem71  44666  fourierdlem73  44668  fourierdlem78  44673  fourierdlem79  44674  fourierdlem80  44675  fourierdlem81  44676  fourierdlem82  44677  fourierdlem83  44678  fourierdlem87  44682  fourierdlem93  44688  fourierdlem95  44690  fourierdlem101  44696  fourierdlem103  44698  fourierdlem104  44699  fourierdlem111  44706  fourierdlem112  44707  sqwvfoura  44717  fourierswlem  44719  elaa2lem  44722  etransclem13  44736  etransclem23  44746  etransclem24  44747  etransclem32  44755  etransclem38  44761  etransclem46  44769  qndenserrnbllem  44783  rrxsnicc  44789  ioorrnopnlem  44793  prsal  44807  intsal  44819  salexct  44823  dfsalgen2  44830  issalnnd  44834  sge0rnre  44853  sge0val  44855  sge0z  44864  sge0revalmpt  44867  sge0tsms  44869  sge0pr  44883  sge0resplit  44895  sge0split  44898  sge0splitmpt  44900  sge0iunmptlemfi  44902  sge0iunmptlemre  44904  sge0fodjrnlem  44905  sge0iunmpt  44907  sge0rpcpnf  44910  sge0ltfirpmpt2  44915  sge0isum  44916  sge0xaddlem1  44922  sge0xaddlem2  44923  sge0pnffsumgt  44931  sge0gtfsumgt  44932  sge0seq  44935  sge0reuz  44936  nnfoctbdjlem  44944  nnfoctbdj  44945  meadjun  44951  meadjiunlem  44954  voliunsge0lem  44961  meaiuninc3v  44973  omeiunltfirp  45008  carageniuncllem2  45011  caratheodorylem1  45015  caratheodorylem2  45016  caratheodory  45017  isomenndlem  45019  isomennd  45020  hoicvr  45037  volicorescl  45042  ovnsubaddlem2  45060  hoidmvlelem2  45085  hoidmvlelem3  45086  hoidmvle  45089  ovnhoilem2  45091  hspdifhsp  45105  hoiqssbllem2  45112  hoiqssbllem3  45113  hspmbllem2  45116  ovnsubadd2lem  45134  ovolval4lem1  45138  vonvolmbl  45150  vonioo  45171  vonicc  45174  pimrecltpos  45197  issmfle  45234  smflimlem1  45260  smflimlem2  45261  smflimlem6  45265  smfresal  45277  smfrec  45278  smfmullem4  45283  smfpimcc  45297  smflimmpt  45299  smfsuplem1  45300  smfsuplem3  45302  smfsupmpt  45304  smfsupxr  45305  smfinflem  45306  smfinfmpt  45308  smflimsuplem4  45312  smflimsuplem5  45313  smflimsupmpt  45318  smfliminfmpt  45321  fsupdm  45331  finfdm  45335  smonoord  45811  lswn0  45884  poprelb  45964  fmtnoprmfac1  46005  fmtnofac2lem  46008  sbgoldbst  46218  resmgmhm  46340  resmgmhm2b  46342  mgmhmco  46343  mgmhmima  46344  snlindsntorlem  46799  1arymaptf  46975  ipolubdm  47260  ipoglbdm  47263  aacllem  47496