Theorem adantll 714

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 580	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  727  ad2ant2l  746  ad2ant2lr  748  ad5ant23  759  ad5ant24  760  ad5ant25  761  3adant1  1130  3ad2antl3  1188  ralcom2  3347  vtocl2d  3519  sbc2iegf  3815  sbcralt  3822  pofun  5550  poinxp  5705  xpdifid  6126  sossfld  6144  preddowncl  6290  tz7.7  6343  onfr  6356  ssimaex  6919  eqfnun  6982  fndmdif  6987  dffo4  7048  fompt  7063  fcompt  7078  fconst2g  7149  f1cofveqaeq  7203  isores3  7281  limsssuc  7792  el2mpocl  8028  1stconst  8042  2ndconst  8043  curry1  8046  curry2  8049  poseq  8100  soseq  8101  extmptsuppeq  8130  suppss  8136  suppss2  8142  onnseq  8276  oe0  8449  oesuclem  8452  oecl  8464  oaordi  8473  oawordri  8477  omordi  8493  omword2  8501  omlimcl  8505  odi  8506  omass  8507  oeoe  8527  nnaordi  8546  oaabs  8576  omsmolem  8585  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  9671  ac5num  9946  cff1  10168  cfcoflem  10182  infpssrlem4  10216  isf32lem9  10271  isf34lem7  10289  fin1a2lem13  10322  fin1a2s  10324  hsmexlem4  10339  axdc2lem  10358  zorn2lem6  10411  axpowndlem2  10509  inttsk  10685  tskuni  10694  nqereu  10840  prcdnq  10904  addclprlem2  10928  ltexpri  10954  prlem936  10958  reclem2pr  10959  axsup  11208  add4  11354  ltleadd  11620  lt2mul2div  12020  nn2ge  12172  zextle  12565  fnn0ind  12591  xrlttr  13054  ifle  13112  xnn0lem1lt  13159  xaddass  13164  xmulasslem3  13201  xlemul1a  13203  xadddilem  13209  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  ixxin  13278  difreicc  13400  iccsplit  13401  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  fzaddel  13474  fzadd2  13475  fzrev  13503  modadd1  13828  modmul1  13847  fsuppmapnn0fiub  13914  mulexp  14024  expadd  14027  expmul  14030  expnbnd  14155  bccl  14245  hashdom  14302  prsshashgt1  14333  hashfacen  14377  brfi1uzind  14431  wrdnval  14468  swrdccat3blem  14662  revccat  14689  2shfti  15003  rexico  15277  cau3lem  15278  subcn2  15518  caucvgb  15603  iseraltlem1  15605  sumss  15647  fsumsplitsn  15667  incexclem  15759  supcvg  15779  mertenslem2  15808  fprodn0  15902  fprodsplitsn  15912  fprodle  15919  eftlcl  16032  reeftlcl  16033  rpnnen2lem6  16144  dvdsext  16248  3dvds  16258  sqoddm1div8z  16281  gcdcllem3  16428  dvdsexpim  16482  bezoutr1  16496  seq1st  16498  dvdslcm  16525  lcmeq0  16527  lcmcl  16528  lcmneg  16530  lcmdvds  16535  coprmgcdb  16576  dvdsprime  16614  pc2dvds  16807  prmpwdvds  16832  unbenlem  16836  infpnlem1  16838  1arith  16855  vdwmc2  16907  ramcl  16957  mrcuni  17544  isacs1i  17580  acsfn  17582  funcpropd  17826  curfcl  18155  curf2ndf  18170  resmgmhm  18636  resmgmhm2b  18638  mgmhmco  18639  mgmhmima  18640  resmhm  18745  resmhm2b  18747  mhmco  18748  pwsdiagmhm  18756  gsumwsubmcl  18762  gsumwspan  18771  pwmnd  18862  dfgrp2  18892  subgint  19080  ghmmhmb  19156  resghm  19161  cntzmhm  19270  symgextf1lem  19349  f1omvdconj  19375  dfod2  19493  gexdvds  19513  subgpgp  19526  sylow1lem3  19529  frgpnabllem1  19802  dprdfeq0  19953  rhmimasubrnglem  20498  cntzsubrng  20500  cntzsubr  20539  isdrng2  20676  islmodd  20817  lsslss  20912  reslmhm2b  21006  rngqiprngimfo  21256  psgnfix1  21553  psgndif  21557  copsgndif  21558  ocvocv  21626  frlmsslsp  21751  frlmlbs  21752  psrbaglefi  21882  psrdi  21920  psrass23l  21922  psrass23  21924  evlsvvval  22048  psdmul  22109  mptcoe1fsupp  22156  psropprmul  22178  ply1coe  22242  rhmcomulmpl  22326  mamudi  22347  mamudir  22348  mat1dimelbas  22415  scmatmulcl  22462  scmatfo  22474  mulmarep1gsum2  22518  mdetunilem7  22562  mdetunilem9  22564  gsummatr01lem3  22601  smadiadetlem3  22612  cpmadugsumlemF  22820  leordtval  23157  cnpnei  23208  cnco  23210  cnss1  23220  cmpsub  23344  hauscmplem  23350  dissnlocfin  23473  ptbasid  23519  tx2cn  23554  upxp  23567  txindis  23578  xkoptsub  23598  xkopt  23599  trfbas2  23787  filconn  23827  trfil2  23831  filssufilg  23855  ufileu  23863  fixufil  23866  ufilen  23874  rnelfmlem  23896  flimclsi  23922  hauspwpwf1  23931  fclsopn  23958  fclsfnflim  23971  fclscmpi  23973  alexsubALTlem4  23994  ptcmplem5  24000  tgpmulg  24037  subgtgp  24049  tgpt0  24063  tsmsxplem2  24098  metss  24452  metustfbas  24501  dscopn  24517  xrsmopn  24757  cncfss  24848  icoopnst  24892  iccpnfcnv  24898  icccvx  24904  evth  24914  phtpycc  24946  pcohtpylem  24975  lmmbrf  25218  fgcfil  25227  caucfil  25239  cfilres  25252  bcth3  25287  cmscsscms  25329  ovolfioo  25424  ovolficc  25425  voliunlem3  25509  volcn  25563  mbflimsup  25623  mbfi1fseqlem5  25676  itg2seq  25699  bddiblnc  25799  dvnff  25881  dvnadd  25887  cpnord  25893  c1liplem1  25957  plypf1  26173  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coeidlem  26198  dgrle  26204  dgrnznn  26208  plycjlem  26238  elqaalem3  26285  ulmcaulem  26359  ulmcau  26360  psergf  26377  psercn2  26388  psercn2OLD  26389  efopn  26623  abscxpbnd  26719  leibpi  26908  isppw2  27081  muinv  27159  bposlem3  27253  gausslemma2dlem4  27336  pntrmax  27531  pntpbnd1  27553  qabvexp  27593  madebday  27896  mulsrid  28109  bdayons  28272  peano5n0s  28315  bdaypw2n0bndlem  28459  bdayfinlem  28482  eqeelen  28977  colinearalglem4  28982  axcgrid  28989  axsegconlem1  28990  axsegconlem3  28992  ax5seglem1  29001  ax5seglem2  29002  ax5seglem9  29010  axcontlem2  29038  cusgrfilem2  29530  vtxdgfisf  29550  usgr2pthlem  29836  uspgrn2crct  29881  crctcshwlkn0  29894  wwlksnext  29966  wwlksnextproplem3  29984  eupth2lem3lem4  30306  frgr3vlem1  30348  frgr3vlem2  30349  3vfriswmgrlem  30352  frgrwopreglem5  30396  numclwwlk3lem2  30459  grpoidinvlem3  30581  grpoidinv  30583  grpoideu  30584  nmoub3i  30848  nmlno0lem  30868  nmlnoubi  30871  ipasslem3  30908  ipblnfi  30930  hvaddsub4  31153  his35  31163  shsel3  31390  chj4  31610  spansncol  31643  chscllem2  31713  5oalem2  31730  3oalem2  31738  hoaddcl  31833  adjsym  31908  cnvadj  31967  hhcno  31979  hhcnf  31980  nmopub2tALT  31984  unoplin  31995  counop  31996  nmfnleub2  32001  hmoplin  32017  brafnmul  32026  nmlnop0iALT  32070  nmopun  32089  nmophmi  32106  riesz3i  32137  riesz1  32140  cnlnadjlem2  32143  cnlnadjlem6  32147  adjmul  32167  adjadd  32168  bra11  32183  cnvbraval  32185  kbass5  32195  kbass6  32196  leop2  32199  leopadd  32207  leopmuli  32208  leoptri  32211  leopnmid  32213  nmopleid  32214  pj3si  32282  hstel2  32294  cvcon3  32359  dmdmd  32375  dmdbr5  32383  mdsl0  32385  mdslmd1lem1  32400  mdslmd1lem2  32401  mdslmd3i  32407  superpos  32429  chirredlem2  32466  chirredlem3  32467  mdsymlem3  32480  mdsymlem5  32482  mdsymlem6  32483  sumdmdlem  32493  cdjreui  32507  cdj1i  32508  cdj3i  32516  foresf1o  32579  2ndimaxp  32724  abfmpel  32733  fcomptf  32736  fcnvgreu  32751  fdifsuppconst  32768  xrge0infss  32840  xnn0gt0  32849  sgn3da  32915  cycpm2tr  33201  elrgspnlem2  33325  elrgspnlem3  33326  intlidl  33501  rhmpreimaprmidl  33532  mplvrpmga  33710  esplyfval0  33722  vieta  33736  lssdimle  33764  mdetpmtr1  33980  cmpcref  34007  xrge0iifcnv  34090  zrhcntr  34136  esumcst  34220  hasheuni  34242  esum2dlem  34249  esum2d  34250  sigaclcu2  34277  insiga  34294  unelldsys  34315  measres  34379  measdivcst  34381  volfiniune  34387  ddemeas  34393  actfunsnf1o  34761  fnrelpredd  35247  fineqvac  35272  fineqvnttrclselem1  35277  sconnpi1  35433  cvmsss2  35468  satfv1lem  35556  fmlaomn0  35584  gonarlem  35588  mrsubco  35715  dfon2lem6  35980  hfext  36377  elicc3  36511  fnessref  36551  bj-ismooredr2  37315  pibt2  37622  fin2solem  37807  fin2so  37808  lindsenlbs  37816  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem2  37823  poimirlem14  37835  poimirlem25  37846  poimirlem26  37847  poimirlem29  37850  poimirlem30  37851  broucube  37855  heicant  37856  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ex-ovoliunnfl  37864  mbfresfi  37867  cnambfre  37869  itg2addnclem  37872  itg2addnclem2  37873  itg2addnc  37875  ftc1anclem3  37896  ftc1anclem4  37897  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  indexdom  37935  filbcmb  37941  fdc  37946  incsequz  37949  metf1o  37956  caures  37961  bndss  37987  ismtycnv  38003  heiborlem1  38012  rrncmslem  38033  isdrngo2  38159  rngoisocnv  38182  unichnidl  38232  erimeq2  38937  ax12eq  39201  ax12el  39202  lshpset2N  39379  pmapglb2N  40031  pmapglb2xN  40032  pclfinN  40160  polval2N  40166  cdleme31fv2  40653  cdleme32fvcl  40700  cdleme48gfv  40797  tendoicl  41056  tendoipl  41057  diaglbN  41315  dochkr1  41738  dochkr1OLDN  41739  sumcubes  42568  expeq1d  42579  zaddcomlem  42718  zmulcomlem  42722  fiabv  42791  rhmcomulpsr  42804  selvcllem5  42825  evlselv  42830  fsuppind  42833  fsuppssind  42836  mhpind  42837  nacsfix  42954  eq0rabdioph  43018  diophren  43055  rencldnfilem  43062  pell1234qrdich  43103  jm2.24  43205  jm2.26lem3  43243  wepwsolem  43284  pwssplit4  43331  isnumbasgrplem3  43347  onexoegt  43486  onov0suclim  43516  cantnfresb  43566  omcl2  43575  ofoaid1  43600  ofoaid2  43601  grumnudlem  44526  cvgdvgrat  44554  ofsubid  44565  bcc0  44581  binomcxplemnn0  44590  uzwo4  45298  fiiuncl  45310  iunincfi  45338  nsstr  45339  rexanuz3  45340  iinssiin  45373  disjrnmpt2  45432  disjinfi  45436  choicefi  45444  fsneq  45450  difmap  45451  iunmapsn  45461  axccdom  45466  axccd  45473  rnmptlb  45487  rnmptbd2lem  45492  ssfiunibd  45557  supxrgelem  45582  suplesup  45584  xrlexaddrp  45597  xralrple2  45599  infxrunb2  45612  xralrple3  45618  xrralrecnnle  45627  xrralrecnnge  45634  supxrunb3  45643  unb2ltle  45659  rexabslelem  45662  supminfrnmpt  45689  infxrpnf  45690  supminfxr  45708  supminfxr2  45713  xrpnf  45729  pimxrneun  45732  cvgcaule  45735  iooiinicc  45788  ressioosup  45801  iooiinioc  45802  ressiooinf  45803  fsumsupp0  45824  divcnvg  45873  limcrecl  45875  sumnnodd  45876  islpcn  45883  lptre2pt  45884  limcresiooub  45886  limcresioolb  45887  limclner  45895  fnlimfvre  45918  allbutfifvre  45919  climinf3  45960  limsupmnflem  45964  limsupre3uzlem  45979  limsupreuzmpt  45983  climuzlem  45987  climisp  45990  climrescn  45992  climxrrelem  45993  climxrre  45994  climlimsupcex  46013  liminflelimsuplem  46019  limsupgtlem  46021  liminfvalxr  46027  liminfreuzlem  46046  liminfltlem  46048  liminflimsupclim  46051  xlimpnfxnegmnf  46058  liminflbuz2  46059  liminflimsupxrre  46061  cnrefiisplem  46073  xlimmnfvlem2  46077  xlimmnfv  46078  xlimpnfvlem2  46081  xlimpnfv  46082  xlimmnfmpt  46087  xlimpnfmpt  46088  climxlim2lem  46089  dfxlim2v  46091  xlimliminflimsup  46106  cncfuni  46130  icccncfext  46131  cncficcgt0  46132  cncfiooicclem1  46137  cncfiooiccre  46139  dvasinbx  46164  dvdsn1add  46183  dvnmul  46187  dvmptfprodlem  46188  dvnprodlem1  46190  dvnprodlem3  46192  iblspltprt  46217  itgioocnicc  46221  itgspltprt  46223  ismbl3  46230  stirlinglem5  46322  dirker2re  46336  dirkerper  46340  dirkertrigeq  46345  dirkercncflem2  46348  fourierdlem12  46363  fourierdlem15  46366  fourierdlem16  46367  fourierdlem20  46371  fourierdlem21  46372  fourierdlem22  46373  fourierdlem39  46390  fourierdlem40  46391  fourierdlem41  46392  fourierdlem42  46393  fourierdlem46  46396  fourierdlem49  46399  fourierdlem50  46400  fourierdlem57  46407  fourierdlem58  46408  fourierdlem59  46409  fourierdlem64  46414  fourierdlem65  46415  fourierdlem66  46416  fourierdlem68  46418  fourierdlem70  46420  fourierdlem71  46421  fourierdlem73  46423  fourierdlem78  46428  fourierdlem79  46429  fourierdlem80  46430  fourierdlem81  46431  fourierdlem82  46432  fourierdlem83  46433  fourierdlem87  46437  fourierdlem93  46443  fourierdlem95  46445  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  sqwvfoura  46472  fourierswlem  46474  elaa2lem  46477  etransclem13  46491  etransclem23  46501  etransclem24  46502  etransclem32  46510  etransclem38  46516  etransclem46  46524  qndenserrnbllem  46538  rrxsnicc  46544  ioorrnopnlem  46548  prsal  46562  intsal  46574  salexct  46578  dfsalgen2  46585  issalnnd  46589  sge0rnre  46608  sge0val  46610  sge0z  46619  sge0revalmpt  46622  sge0tsms  46624  sge0pr  46638  sge0resplit  46650  sge0split  46653  sge0splitmpt  46655  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0fodjrnlem  46660  sge0iunmpt  46662  sge0rpcpnf  46665  sge0ltfirpmpt2  46670  sge0isum  46671  sge0xaddlem1  46677  sge0xaddlem2  46678  sge0pnffsumgt  46686  sge0gtfsumgt  46687  sge0seq  46690  sge0reuz  46691  nnfoctbdjlem  46699  nnfoctbdj  46700  meadjun  46706  meadjiunlem  46709  voliunsge0lem  46716  meaiuninc3v  46728  omeiunltfirp  46763  carageniuncllem2  46766  caratheodorylem1  46770  caratheodorylem2  46771  caratheodory  46772  isomenndlem  46774  isomennd  46775  hoicvr  46792  volicorescl  46797  ovnsubaddlem2  46815  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvle  46844  ovnhoilem2  46846  hspdifhsp  46860  hoiqssbllem2  46867  hoiqssbllem3  46868  hspmbllem2  46871  ovnsubadd2lem  46889  ovolval4lem1  46893  vonvolmbl  46905  vonioo  46926  vonicc  46929  pimrecltpos  46952  issmfle  46989  smflimlem1  47015  smflimlem2  47016  smflimlem6  47020  smfresal  47032  smfrec  47033  smfmullem4  47038  smfpimcc  47052  smflimmpt  47054  smfsuplem1  47055  smfsuplem3  47057  smfsupmpt  47059  smfsupxr  47060  smfinflem  47061  smfinfmpt  47063  smflimsuplem4  47067  smflimsuplem5  47068  smflimsupmpt  47073  smfliminfmpt  47076  fsupdm  47086  finfdm  47090  smonoord  47617  lswn0  47690  poprelb  47770  fmtnoprmfac1  47811  fmtnofac2lem  47814  sbgoldbst  48024  isgrim  48128  gpgedgvtx0  48307  snlindsntorlem  48716  1arymaptf  48887  ipolubdm  49232  ipoglbdm  49235  setc1onsubc  49847  aacllem  50046