Theorem adantll 715

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad2antlr  728  ad2ant2l  747  ad2ant2lr  749  ad5ant23  760  ad5ant24  761  ad5ant25  762  3adant1  1131  3ad2antl3  1189  ralcom2  3339  vtocl2d  3507  sbc2iegf  3803  sbcralt  3810  pofun  5557  poinxp  5712  xpdifid  6132  sossfld  6150  preddowncl  6296  tz7.7  6349  onfr  6362  ssimaex  6925  eqfnun  6989  fndmdif  6994  dffo4  7055  fompt  7070  fcompt  7086  fconst2g  7158  f1cofveqaeq  7212  isores3  7290  limsssuc  7801  el2mpocl  8036  1stconst  8050  2ndconst  8051  curry1  8054  curry2  8057  poseq  8108  soseq  8109  extmptsuppeq  8138  suppss  8144  suppss2  8150  onnseq  8284  oe0  8457  oesuclem  8460  oecl  8472  oaordi  8481  oawordri  8485  omordi  8501  omword2  8509  omlimcl  8513  odi  8514  omass  8515  oeoe  8535  nnaordi  8554  oaabs  8584  omsmolem  8593  eceqoveq  8769  mapsnd  8834  dom2lem  8939  sbthlem9  9033  rexdif1en  9095  isinf  9175  frfi  9195  fiint  9237  fodomfib  9239  fodomfibOLD  9241  fofinf1o  9242  marypha1lem  9346  ordiso2  9430  unwdomg  9499  xpwdomg  9500  frr1  9683  ac5num  9958  cff1  10180  cfcoflem  10194  infpssrlem4  10228  isf32lem9  10283  isf34lem7  10301  fin1a2lem13  10334  fin1a2s  10336  hsmexlem4  10351  axdc2lem  10370  zorn2lem6  10423  axpowndlem2  10521  inttsk  10697  tskuni  10706  nqereu  10852  prcdnq  10916  addclprlem2  10940  ltexpri  10966  prlem936  10970  reclem2pr  10971  axsup  11221  add4  11367  ltleadd  11633  lt2mul2div  12034  nn2ge  12204  zextle  12602  fnn0ind  12628  xrlttr  13091  ifle  13149  xnn0lem1lt  13196  xaddass  13201  xmulasslem3  13238  xlemul1a  13240  xadddilem  13246  xrsupsslem  13259  xrinfmsslem  13260  supxrunb1  13271  supxrunb2  13272  ixxin  13315  difreicc  13437  iccsplit  13438  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  fzaddel  13512  fzadd2  13513  fzrev  13541  modadd1  13867  modmul1  13886  fsuppmapnn0fiub  13953  mulexp  14063  expadd  14066  expmul  14069  expnbnd  14194  bccl  14284  hashdom  14341  prsshashgt1  14372  hashfacen  14416  brfi1uzind  14470  wrdnval  14507  swrdccat3blem  14701  revccat  14728  2shfti  15042  rexico  15316  cau3lem  15317  subcn2  15557  caucvgb  15642  iseraltlem1  15644  sumss  15686  fsumsplitsn  15706  incexclem  15801  supcvg  15821  mertenslem2  15850  fprodn0  15944  fprodsplitsn  15954  fprodle  15961  eftlcl  16074  reeftlcl  16075  rpnnen2lem6  16186  dvdsext  16290  3dvds  16300  sqoddm1div8z  16323  gcdcllem3  16470  dvdsexpim  16524  bezoutr1  16538  seq1st  16540  dvdslcm  16567  lcmeq0  16569  lcmcl  16570  lcmneg  16572  lcmdvds  16577  coprmgcdb  16618  dvdsprime  16656  pc2dvds  16850  prmpwdvds  16875  unbenlem  16879  infpnlem1  16881  1arith  16898  vdwmc2  16950  ramcl  17000  mrcuni  17587  isacs1i  17623  acsfn  17625  funcpropd  17869  curfcl  18198  curf2ndf  18213  resmgmhm  18679  resmgmhm2b  18681  mgmhmco  18682  mgmhmima  18683  resmhm  18788  resmhm2b  18790  mhmco  18791  pwsdiagmhm  18799  gsumwsubmcl  18805  gsumwspan  18814  pwmnd  18908  dfgrp2  18938  subgint  19126  ghmmhmb  19202  resghm  19207  cntzmhm  19316  symgextf1lem  19395  f1omvdconj  19421  dfod2  19539  gexdvds  19559  subgpgp  19572  sylow1lem3  19575  frgpnabllem1  19848  dprdfeq0  19999  rhmimasubrnglem  20542  cntzsubrng  20544  cntzsubr  20583  isdrng2  20720  islmodd  20861  lsslss  20956  reslmhm2b  21049  rngqiprngimfo  21299  psgnfix1  21578  psgndif  21582  copsgndif  21583  ocvocv  21651  frlmsslsp  21776  frlmlbs  21777  psrbaglefi  21906  psrdi  21943  psrass23l  21945  psrass23  21947  evlsvvval  22071  psdmul  22132  mptcoe1fsupp  22179  psropprmul  22201  ply1coe  22263  rhmcomulmpl  22347  mamudi  22368  mamudir  22369  mat1dimelbas  22436  scmatmulcl  22483  scmatfo  22495  mulmarep1gsum2  22539  mdetunilem7  22583  mdetunilem9  22585  gsummatr01lem3  22622  smadiadetlem3  22633  cpmadugsumlemF  22841  leordtval  23178  cnpnei  23229  cnco  23231  cnss1  23241  cmpsub  23365  hauscmplem  23371  dissnlocfin  23494  ptbasid  23540  tx2cn  23575  upxp  23588  txindis  23599  xkoptsub  23619  xkopt  23620  trfbas2  23808  filconn  23848  trfil2  23852  filssufilg  23876  ufileu  23884  fixufil  23887  ufilen  23895  rnelfmlem  23917  flimclsi  23943  hauspwpwf1  23952  fclsopn  23979  fclsfnflim  23992  fclscmpi  23994  alexsubALTlem4  24015  ptcmplem5  24021  tgpmulg  24058  subgtgp  24070  tgpt0  24084  tsmsxplem2  24119  metss  24473  metustfbas  24522  dscopn  24538  xrsmopn  24778  cncfss  24866  icoopnst  24906  iccpnfcnv  24911  icccvx  24917  evth  24926  phtpycc  24958  pcohtpylem  24986  lmmbrf  25229  fgcfil  25238  caucfil  25250  cfilres  25263  bcth3  25298  cmscsscms  25340  ovolfioo  25434  ovolficc  25435  voliunlem3  25519  volcn  25573  mbflimsup  25633  mbfi1fseqlem5  25686  itg2seq  25709  bddiblnc  25809  dvnff  25890  dvnadd  25896  cpnord  25902  c1liplem1  25963  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  dgrle  26208  dgrnznn  26212  plycjlem  26241  elqaalem3  26287  ulmcaulem  26359  ulmcau  26360  psergf  26377  psercn2  26388  efopn  26622  abscxpbnd  26717  leibpi  26906  isppw2  27078  muinv  27156  bposlem3  27249  gausslemma2dlem4  27332  pntrmax  27527  pntpbnd1  27549  qabvexp  27589  madebday  27892  mulsrid  28105  bdayons  28268  peano5n0s  28311  bdaypw2n0bndlem  28455  bdayfinlem  28478  eqeelen  28973  colinearalglem4  28978  axcgrid  28985  axsegconlem1  28986  axsegconlem3  28988  ax5seglem1  28997  ax5seglem2  28998  ax5seglem9  29006  axcontlem2  29034  cusgrfilem2  29525  vtxdgfisf  29545  usgr2pthlem  29831  uspgrn2crct  29876  crctcshwlkn0  29889  wwlksnext  29961  wwlksnextproplem3  29979  eupth2lem3lem4  30301  frgr3vlem1  30343  frgr3vlem2  30344  3vfriswmgrlem  30347  frgrwopreglem5  30391  numclwwlk3lem2  30454  grpoidinvlem3  30577  grpoidinv  30579  grpoideu  30580  nmoub3i  30844  nmlno0lem  30864  nmlnoubi  30867  ipasslem3  30904  ipblnfi  30926  hvaddsub4  31149  his35  31159  shsel3  31386  chj4  31606  spansncol  31639  chscllem2  31709  5oalem2  31726  3oalem2  31734  hoaddcl  31829  adjsym  31904  cnvadj  31963  hhcno  31975  hhcnf  31976  nmopub2tALT  31980  unoplin  31991  counop  31992  nmfnleub2  31997  hmoplin  32013  brafnmul  32022  nmlnop0iALT  32066  nmopun  32085  nmophmi  32102  riesz3i  32133  riesz1  32136  cnlnadjlem2  32139  cnlnadjlem6  32143  adjmul  32163  adjadd  32164  bra11  32179  cnvbraval  32181  kbass5  32191  kbass6  32192  leop2  32195  leopadd  32203  leopmuli  32204  leoptri  32207  leopnmid  32209  nmopleid  32210  pj3si  32278  hstel2  32290  cvcon3  32355  dmdmd  32371  dmdbr5  32379  mdsl0  32381  mdslmd1lem1  32396  mdslmd1lem2  32397  mdslmd3i  32403  superpos  32425  chirredlem2  32462  chirredlem3  32463  mdsymlem3  32476  mdsymlem5  32478  mdsymlem6  32479  sumdmdlem  32489  cdjreui  32503  cdj1i  32504  cdj3i  32512  foresf1o  32574  2ndimaxp  32719  abfmpel  32728  fcomptf  32731  fcnvgreu  32745  fdifsuppconst  32762  xrge0infss  32833  xnn0gt0  32842  sgn3da  32907  cycpm2tr  33180  elrgspnlem2  33304  elrgspnlem3  33305  intlidl  33480  rhmpreimaprmidl  33511  mplvrpmga  33689  psrmonmul  33694  esplyfval0  33708  vieta  33724  lssdimle  33752  mdetpmtr1  33967  cmpcref  33994  xrge0iifcnv  34077  zrhcntr  34123  esumcst  34207  hasheuni  34229  esum2dlem  34236  esum2d  34237  sigaclcu2  34264  insiga  34281  unelldsys  34302  measres  34366  measdivcst  34368  volfiniune  34374  ddemeas  34380  actfunsnf1o  34748  fnrelpredd  35234  fineqvac  35260  fineqvnttrclselem1  35265  sconnpi1  35421  cvmsss2  35456  satfv1lem  35544  fmlaomn0  35572  gonarlem  35576  mrsubco  35703  dfon2lem6  35968  hfext  36365  elicc3  36499  fnessref  36539  bj-ismooredr2  37422  pibt2  37733  fin2solem  37927  fin2so  37928  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem2  37943  poimirlem14  37955  poimirlem25  37966  poimirlem26  37967  poimirlem29  37970  poimirlem30  37971  broucube  37975  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ex-ovoliunnfl  37984  mbfresfi  37987  cnambfre  37989  itg2addnclem  37992  itg2addnclem2  37993  itg2addnc  37995  ftc1anclem3  38016  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  indexdom  38055  filbcmb  38061  fdc  38066  incsequz  38069  metf1o  38076  caures  38081  bndss  38107  ismtycnv  38123  heiborlem1  38132  rrncmslem  38153  isdrngo2  38279  rngoisocnv  38302  unichnidl  38352  erimeq2  39084  ax12eq  39387  ax12el  39388  lshpset2N  39565  pmapglb2N  40217  pmapglb2xN  40218  pclfinN  40346  polval2N  40352  cdleme31fv2  40839  cdleme32fvcl  40886  cdleme48gfv  40983  tendoicl  41242  tendoipl  41243  diaglbN  41501  dochkr1  41924  dochkr1OLDN  41925  sumcubes  42745  expeq1d  42756  zaddcomlem  42908  zmulcomlem  42912  fiabv  42981  rhmcomulpsr  42994  selvcllem5  43015  evlselv  43020  fsuppind  43023  fsuppssind  43026  mhpind  43027  nacsfix  43144  eq0rabdioph  43208  diophren  43241  rencldnfilem  43248  pell1234qrdich  43289  jm2.24  43391  jm2.26lem3  43429  wepwsolem  43470  pwssplit4  43517  isnumbasgrplem3  43533  onexoegt  43672  onov0suclim  43702  cantnfresb  43752  omcl2  43761  ofoaid1  43786  ofoaid2  43787  grumnudlem  44712  cvgdvgrat  44740  ofsubid  44751  bcc0  44767  binomcxplemnn0  44776  uzwo4  45484  fiiuncl  45496  iunincfi  45524  nsstr  45525  rexanuz3  45526  iinssiin  45559  disjrnmpt2  45618  disjinfi  45622  choicefi  45629  fsneq  45635  difmap  45636  iunmapsn  45646  axccdom  45651  axccd  45658  rnmptlb  45672  rnmptbd2lem  45677  ssfiunibd  45742  supxrgelem  45767  suplesup  45769  xrlexaddrp  45782  xralrple2  45784  infxrunb2  45797  xralrple3  45803  xrralrecnnle  45812  xrralrecnnge  45819  supxrunb3  45828  unb2ltle  45843  rexabslelem  45846  supminfrnmpt  45873  infxrpnf  45874  supminfxr  45892  supminfxr2  45897  xrpnf  45913  pimxrneun  45916  cvgcaule  45919  iooiinicc  45972  ressioosup  45985  iooiinioc  45986  ressiooinf  45987  fsumsupp0  46008  divcnvg  46057  limcrecl  46059  sumnnodd  46060  islpcn  46067  lptre2pt  46068  limcresiooub  46070  limcresioolb  46071  limclner  46079  fnlimfvre  46102  allbutfifvre  46103  climinf3  46144  limsupmnflem  46148  limsupre3uzlem  46163  limsupreuzmpt  46167  climuzlem  46171  climisp  46174  climrescn  46176  climxrrelem  46177  climxrre  46178  climlimsupcex  46197  liminflelimsuplem  46203  limsupgtlem  46205  liminfvalxr  46211  liminfreuzlem  46230  liminfltlem  46232  liminflimsupclim  46235  xlimpnfxnegmnf  46242  liminflbuz2  46243  liminflimsupxrre  46245  cnrefiisplem  46257  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  xlimmnfmpt  46271  xlimpnfmpt  46272  climxlim2lem  46273  dfxlim2v  46275  xlimliminflimsup  46290  cncfuni  46314  icccncfext  46315  cncficcgt0  46316  cncfiooicclem1  46321  cncfiooiccre  46323  dvasinbx  46348  dvdsn1add  46367  dvnmul  46371  dvmptfprodlem  46372  dvnprodlem1  46374  dvnprodlem3  46376  iblspltprt  46401  itgioocnicc  46405  itgspltprt  46407  ismbl3  46414  stirlinglem5  46506  dirker2re  46520  dirkerper  46524  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem12  46547  fourierdlem15  46550  fourierdlem16  46551  fourierdlem20  46555  fourierdlem21  46556  fourierdlem22  46557  fourierdlem39  46574  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem46  46580  fourierdlem49  46583  fourierdlem50  46584  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem64  46598  fourierdlem65  46599  fourierdlem66  46600  fourierdlem68  46602  fourierdlem70  46604  fourierdlem71  46605  fourierdlem73  46607  fourierdlem78  46612  fourierdlem79  46613  fourierdlem80  46614  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem87  46621  fourierdlem93  46627  fourierdlem95  46629  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  sqwvfoura  46656  fourierswlem  46658  elaa2lem  46661  etransclem13  46675  etransclem23  46685  etransclem24  46686  etransclem32  46694  etransclem38  46700  etransclem46  46708  qndenserrnbllem  46722  rrxsnicc  46728  ioorrnopnlem  46732  prsal  46746  intsal  46758  salexct  46762  dfsalgen2  46769  issalnnd  46773  sge0rnre  46792  sge0val  46794  sge0z  46803  sge0revalmpt  46806  sge0tsms  46808  sge0pr  46822  sge0resplit  46834  sge0split  46837  sge0splitmpt  46839  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0fodjrnlem  46844  sge0iunmpt  46846  sge0rpcpnf  46849  sge0ltfirpmpt2  46854  sge0isum  46855  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0pnffsumgt  46870  sge0gtfsumgt  46871  sge0seq  46874  sge0reuz  46875  nnfoctbdjlem  46883  nnfoctbdj  46884  meadjun  46890  meadjiunlem  46893  voliunsge0lem  46900  meaiuninc3v  46912  omeiunltfirp  46947  carageniuncllem2  46950  caratheodorylem1  46954  caratheodorylem2  46955  caratheodory  46956  isomenndlem  46958  isomennd  46959  hoicvr  46976  volicorescl  46981  ovnsubaddlem2  46999  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvle  47028  ovnhoilem2  47030  hspdifhsp  47044  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem2  47055  ovnsubadd2lem  47073  ovolval4lem1  47077  vonvolmbl  47089  vonioo  47110  vonicc  47113  pimrecltpos  47136  issmfle  47173  smflimlem1  47199  smflimlem2  47200  smflimlem6  47204  smfresal  47216  smfrec  47217  smfmullem4  47222  smfpimcc  47236  smflimmpt  47238  smfsuplem1  47239  smfsuplem3  47241  smfsupmpt  47243  smfsupxr  47244  smfinflem  47245  smfinfmpt  47247  smflimsuplem4  47251  smflimsuplem5  47252  smflimsupmpt  47257  smfliminfmpt  47260  fsupdm  47270  finfdm  47274  smonoord  47825  lswn0  47904  poprelb  47984  fmtnoprmfac1  48028  fmtnofac2lem  48031  sbgoldbst  48254  isgrim  48358  gpgedgvtx0  48537  snlindsntorlem  48946  1arymaptf  49117  ipolubdm  49462  ipoglbdm  49465  setc1onsubc  50077  aacllem  50276