Theorem adantll 710

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 579	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 206  df-an 396

This theorem is referenced by:  ad2antlr  723  ad2ant2l  742  ad2ant2lr  744  ad5ant23  756  ad5ant24  757  ad5ant25  758  3adant1  1128  3ad2antl3  1185  ralcom2  3288  ralimda  3421  vtocl2d  3486  sbc2iegf  3794  sbcralt  3801  pofun  5512  poinxp  5658  xpdifid  6060  sossfld  6078  preddowncl  6224  tz7.7  6277  onfr  6290  ssimaex  6835  fndmdif  6901  dffo4  6961  fcompt  6987  fconst2g  7060  f1cofveqaeq  7112  2f1fvneq  7114  isores3  7186  fvmptopab  7308  limsssuc  7672  el2mpocl  7897  1stconst  7911  2ndconst  7912  curry1  7915  curry2  7918  extmptsuppeq  7975  suppss  7981  suppssOLD  7982  suppssov1  7985  suppss2  7987  onnseq  8146  oe0  8314  oesuclem  8317  oecl  8329  oaordi  8339  oawordri  8343  omordi  8359  omword2  8367  omlimcl  8371  odi  8372  omass  8373  oeoe  8392  nnaordi  8411  oaabs  8438  omsmolem  8447  eceqoveq  8569  mapsnd  8632  dom2lem  8735  sbthlem9  8831  php3  8899  onomeneq  8943  isinf  8965  frfi  8989  fiint  9021  fodomfib  9023  fofinf1o  9024  marypha1lem  9122  ordiso2  9204  unwdomg  9273  xpwdomg  9274  dftrpred3g  9412  frr1  9448  ac5num  9723  cff1  9945  cfcoflem  9959  infpssrlem4  9993  isf32lem9  10048  isf34lem7  10066  fin1a2lem13  10099  fin1a2s  10101  hsmexlem4  10116  axdc2lem  10135  zorn2lem6  10188  axpowndlem2  10285  inttsk  10461  tskuni  10470  nqereu  10616  prcdnq  10680  addclprlem2  10704  ltexpri  10730  prlem936  10734  reclem2pr  10735  axsup  10981  add4  11125  ltleadd  11388  lt2mul2div  11783  nn2ge  11930  zextle  12323  fnn0ind  12349  xrlttr  12803  ifle  12860  xnn0lem1lt  12907  xaddass  12912  xmulasslem3  12949  xlemul1a  12951  xadddilem  12957  xrsupsslem  12970  xrinfmsslem  12971  supxrunb1  12982  supxrunb2  12983  ixxin  13025  difreicc  13145  iccsplit  13146  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  fzaddel  13219  fzadd2  13220  fzrev  13248  modadd1  13556  modmul1  13572  fsuppmapnn0fiub  13639  mulexp  13750  expadd  13753  expmul  13756  expnbnd  13875  bccl  13964  hashdom  14022  prsshashgt1  14053  hashfacen  14094  hashfacenOLD  14095  brfi1uzind  14140  wrdnval  14176  swrdccat3blem  14380  revccat  14407  2shfti  14719  rexico  14993  cau3lem  14994  subcn2  15232  caucvgb  15319  iseraltlem1  15321  sumss  15364  fsumsplitsn  15384  incexclem  15476  supcvg  15496  mertenslem2  15525  fprodn0  15617  fprodsplitsn  15627  fprodle  15634  eftlcl  15744  reeftlcl  15745  rpnnen2lem6  15856  dvdsext  15958  3dvds  15968  sqoddm1div8z  15991  gcdcllem3  16136  bezoutr1  16202  seq1st  16204  dvdslcm  16231  lcmeq0  16233  lcmcl  16234  lcmneg  16236  lcmdvds  16241  coprmgcdb  16282  dvdsprime  16320  pc2dvds  16508  prmpwdvds  16533  unbenlem  16537  infpnlem1  16539  1arith  16556  vdwmc2  16608  ramcl  16658  mrcuni  17247  isacs1i  17283  acsfn  17285  funcpropd  17532  curfcl  17866  curf2ndf  17881  resmhm  18374  resmhm2b  18376  mhmco  18377  mhmima  18378  pwsdiagmhm  18384  gsumwsubmcl  18390  gsumwspan  18400  pwmnd  18491  dfgrp2  18519  subgint  18694  ghmmhmb  18760  resghm  18765  cntzmhm  18860  symgextf1lem  18943  f1omvdconj  18969  dfod2  19086  gexdvds  19104  subgpgp  19117  sylow1lem3  19120  frgpnabllem1  19389  dprdfeq0  19540  isdrng2  19916  cntzsubr  19972  islmodd  20044  lsslss  20138  reslmhm2b  20231  psgnfix1  20715  psgndif  20719  copsgndif  20720  ocvocv  20788  frlmsslsp  20913  frlmlbs  20914  psrbaglefi  21045  psrbaglefiOLD  21046  mptcoe1fsupp  21296  psropprmul  21319  ply1coe  21377  mamudi  21460  mamudir  21461  mat1dimelbas  21528  scmatmulcl  21575  scmatfo  21587  mulmarep1gsum2  21631  mdetunilem7  21675  mdetunilem9  21677  gsummatr01lem3  21714  smadiadetlem3  21725  cpmadugsumlemF  21933  leordtval  22272  cnpnei  22323  cnco  22325  cnss1  22335  cmpsub  22459  hauscmplem  22465  dissnlocfin  22588  ptbasid  22634  tx2cn  22669  upxp  22682  txindis  22693  xkoptsub  22713  xkopt  22714  trfbas2  22902  filconn  22942  trfil2  22946  filssufilg  22970  ufileu  22978  fixufil  22981  ufilen  22989  rnelfmlem  23011  flimclsi  23037  hauspwpwf1  23046  fclsopn  23073  fclsfnflim  23086  fclscmpi  23088  alexsubALTlem4  23109  ptcmplem5  23115  tgpmulg  23152  subgtgp  23164  tgpt0  23178  tsmsxplem2  23213  metss  23570  metustfbas  23619  dscopn  23635  xrsmopn  23881  cncfss  23968  icoopnst  24008  iccpnfcnv  24013  icccvx  24019  evth  24028  phtpycc  24060  pcohtpylem  24088  lmmbrf  24331  fgcfil  24340  caucfil  24352  cfilres  24365  bcth3  24400  cmscsscms  24442  ovolfioo  24536  ovolficc  24537  voliunlem3  24621  volcn  24675  mbflimsup  24735  mbfi1fseqlem5  24789  itg2seq  24812  bddiblnc  24911  dvnff  24992  dvnadd  24998  cpnord  25004  c1liplem1  25065  plypf1  25278  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  coeidlem  25303  dgrle  25309  dgrnznn  25313  plycjlem  25342  elqaalem3  25386  ulmcaulem  25458  ulmcau  25459  psergf  25476  psercn2  25487  efopn  25718  abscxpbnd  25811  leibpi  25997  isppw2  26169  muinv  26247  bposlem3  26339  gausslemma2dlem4  26422  pntrmax  26617  pntpbnd1  26639  qabvexp  26679  eqeelen  27175  colinearalglem4  27180  axcgrid  27187  axsegconlem1  27188  axsegconlem3  27190  ax5seglem1  27199  ax5seglem2  27200  ax5seglem9  27208  axcontlem2  27236  cusgrfilem2  27726  vtxdgfisf  27746  usgr2pthlem  28032  uspgrn2crct  28074  crctcshwlkn0  28087  wwlksnext  28159  wwlksnextproplem3  28177  eupth2lem3lem4  28496  frgr3vlem1  28538  frgr3vlem2  28539  3vfriswmgrlem  28542  frgrwopreglem5  28586  numclwwlk3lem2  28649  grpoidinvlem3  28769  grpoidinv  28771  grpoideu  28772  nmoub3i  29036  nmlno0lem  29056  nmlnoubi  29059  ipasslem3  29096  ipblnfi  29118  hvaddsub4  29341  his35  29351  shsel3  29578  chj4  29798  spansncol  29831  chscllem2  29901  5oalem2  29918  3oalem2  29926  hoaddcl  30021  adjsym  30096  cnvadj  30155  hhcno  30167  hhcnf  30168  nmopub2tALT  30172  unoplin  30183  counop  30184  nmfnleub2  30189  hmoplin  30205  brafnmul  30214  nmlnop0iALT  30258  nmopun  30277  nmophmi  30294  riesz3i  30325  riesz1  30328  cnlnadjlem2  30331  cnlnadjlem6  30335  adjmul  30355  adjadd  30356  bra11  30371  cnvbraval  30373  kbass5  30383  kbass6  30384  leop2  30387  leopadd  30395  leopmuli  30396  leoptri  30399  leopnmid  30401  nmopleid  30402  pj3si  30470  hstel2  30482  cvcon3  30547  dmdmd  30563  dmdbr5  30571  mdsl0  30573  mdslmd1lem1  30588  mdslmd1lem2  30589  mdslmd3i  30595  superpos  30617  chirredlem2  30654  chirredlem3  30655  mdsymlem3  30668  mdsymlem5  30670  mdsymlem6  30671  sumdmdlem  30681  cdjreui  30695  cdj1i  30696  cdj3i  30704  foresf1o  30751  2ndimaxp  30885  abfmpel  30894  fcomptf  30897  fcnvgreu  30912  fdifsuppconst  30925  xrge0infss  30985  xnn0gt0  30994  cycpm2tr  31288  intlidl  31504  rhmpreimaprmidl  31529  lssdimle  31593  mdetpmtr1  31675  cmpcref  31702  xrge0iifcnv  31785  esumcst  31931  hasheuni  31953  esum2dlem  31960  esum2d  31961  sigaclcu2  31988  insiga  32005  unelldsys  32026  measres  32090  measdivcst  32092  volfiniune  32098  ddemeas  32104  sgn3da  32408  actfunsnf1o  32484  fnrelpredd  32961  fineqvac  32966  sconnpi1  33101  cvmsss2  33136  satfv1lem  33224  fmlaomn0  33252  gonarlem  33256  mrsubco  33383  dfon2lem6  33670  poseq  33729  soseq  33730  madebday  34007  hfext  34412  elicc3  34433  fnessref  34473  bj-ismooredr2  35208  pibt2  35515  fin2solem  35690  fin2so  35691  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem2  35706  poimirlem14  35718  poimirlem25  35729  poimirlem26  35730  poimirlem29  35733  poimirlem30  35734  broucube  35738  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ex-ovoliunnfl  35747  mbfresfi  35750  cnambfre  35752  itg2addnclem  35755  itg2addnclem2  35756  itg2addnc  35758  ftc1anclem3  35779  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  eqfnun  35807  indexdom  35819  filbcmb  35825  fdc  35830  incsequz  35833  metf1o  35840  caures  35845  bndss  35871  ismtycnv  35887  heiborlem1  35896  rrncmslem  35917  isdrngo2  36043  rngoisocnv  36066  unichnidl  36116  erim2  36716  ax12eq  36882  ax12el  36883  lshpset2N  37060  pmapglb2N  37712  pmapglb2xN  37713  pclfinN  37841  polval2N  37847  cdleme31fv2  38334  cdleme32fvcl  38381  cdleme48gfv  38478  tendoicl  38737  tendoipl  38738  diaglbN  38996  dochkr1  39419  dochkr1OLDN  39420  selvval2lem5  40155  fsuppind  40202  fsuppssind  40205  mhpind  40206  dvdsexpim  40249  nacsfix  40450  eq0rabdioph  40514  diophren  40551  rencldnfilem  40558  pell1234qrdich  40599  jm2.24  40701  jm2.26lem3  40739  wepwsolem  40783  pwssplit4  40830  isnumbasgrplem3  40846  grumnudlem  41792  cvgdvgrat  41820  ofsubid  41831  bcc0  41847  binomcxplemnn0  41856  uzwo4  42490  fiiuncl  42502  iunincfi  42533  nsstr  42534  rexanuz3  42535  iinssiin  42567  disjrnmpt2  42615  fompt  42619  disjinfi  42620  choicefi  42629  fsneq  42635  difmap  42636  iunmapsn  42646  axccdom  42651  axccd  42657  rnmptlb  42677  rnmptbd2lem  42683  ssfiunibd  42738  supxrgelem  42766  suplesup  42768  xrlexaddrp  42781  xralrple2  42783  infxrunb2  42797  xralrple3  42803  xrralrecnnle  42812  xrralrecnnge  42820  supxrunb3  42829  unb2ltle  42845  rexabslelem  42848  supminfrnmpt  42875  infxrpnf  42876  supminfxr  42894  supminfxr2  42899  xrpnf  42916  iooiinicc  42970  ressioosup  42983  iooiinioc  42984  ressiooinf  42985  fsumsupp0  43009  divcnvg  43058  limcrecl  43060  sumnnodd  43061  islpcn  43070  lptre2pt  43071  limcresiooub  43073  limcresioolb  43074  limclner  43082  fnlimfvre  43105  allbutfifvre  43106  climinf3  43147  limsupmnflem  43151  limsupre3uzlem  43166  limsupreuzmpt  43170  climuzlem  43174  climisp  43177  climrescn  43179  climxrrelem  43180  climxrre  43181  climlimsupcex  43200  liminflelimsuplem  43206  limsupgtlem  43208  liminfvalxr  43214  liminfreuzlem  43233  liminfltlem  43235  liminflimsupclim  43238  xlimpnfxnegmnf  43245  liminflbuz2  43246  liminflimsupxrre  43248  cnrefiisplem  43260  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem2  43268  xlimpnfv  43269  xlimmnfmpt  43274  xlimpnfmpt  43275  climxlim2lem  43276  dfxlim2v  43278  xlimliminflimsup  43293  cncfuni  43317  icccncfext  43318  cncficcgt0  43319  cncfiooicclem1  43324  cncfiooiccre  43326  dvasinbx  43351  dvdsn1add  43370  dvnmul  43374  dvmptfprodlem  43375  dvnprodlem1  43377  dvnprodlem3  43379  iblspltprt  43404  itgioocnicc  43408  itgspltprt  43410  ismbl3  43417  stirlinglem5  43509  dirker2re  43523  dirkerper  43527  dirkertrigeq  43532  dirkercncflem2  43535  fourierdlem12  43550  fourierdlem15  43553  fourierdlem16  43554  fourierdlem20  43558  fourierdlem21  43559  fourierdlem22  43560  fourierdlem39  43577  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem46  43583  fourierdlem49  43586  fourierdlem50  43587  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem64  43601  fourierdlem65  43602  fourierdlem66  43603  fourierdlem68  43605  fourierdlem70  43607  fourierdlem71  43608  fourierdlem73  43610  fourierdlem78  43615  fourierdlem79  43616  fourierdlem80  43617  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem87  43624  fourierdlem93  43630  fourierdlem95  43632  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  sqwvfoura  43659  fourierswlem  43661  elaa2lem  43664  etransclem13  43678  etransclem23  43688  etransclem24  43689  etransclem32  43697  etransclem38  43703  etransclem46  43711  qndenserrnbllem  43725  rrxsnicc  43731  ioorrnopnlem  43735  prsal  43749  intsal  43759  salexct  43763  dfsalgen2  43770  issalnnd  43774  sge0rnre  43792  sge0val  43794  sge0z  43803  sge0revalmpt  43806  sge0tsms  43808  sge0pr  43822  sge0resplit  43834  sge0split  43837  sge0splitmpt  43839  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0iunmpt  43846  sge0rpcpnf  43849  sge0ltfirpmpt2  43854  sge0isum  43855  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0pnffsumgt  43870  sge0gtfsumgt  43871  sge0seq  43874  sge0reuz  43875  nnfoctbdjlem  43883  nnfoctbdj  43884  meadjun  43890  meadjiunlem  43893  voliunsge0lem  43900  meaiuninc3v  43912  omeiunltfirp  43947  carageniuncllem2  43950  caratheodorylem1  43954  caratheodorylem2  43955  caratheodory  43956  isomenndlem  43958  isomennd  43959  hoicvr  43976  volicorescl  43981  ovnsubaddlem2  43999  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvle  44028  ovnhoilem2  44030  hspdifhsp  44044  hoiqssbllem2  44051  hoiqssbllem3  44052  hspmbllem2  44055  ovnsubadd2lem  44073  ovolval4lem1  44077  vonvolmbl  44089  vonioo  44110  vonicc  44113  pimrecltpos  44133  issmfle  44168  smflimlem1  44193  smflimlem2  44194  smflimlem6  44198  smfresal  44209  smfrec  44210  smfmullem4  44215  smfpimcc  44228  smflimmpt  44230  smfsuplem1  44231  smfsuplem3  44233  smfsupmpt  44235  smfsupxr  44236  smfinflem  44237  smfinfmpt  44239  smflimsuplem4  44243  smflimsuplem5  44244  smflimsupmpt  44249  smfliminfmpt  44252  smonoord  44711  lswn0  44784  poprelb  44864  fmtnoprmfac1  44905  fmtnofac2lem  44908  sbgoldbst  45118  resmgmhm  45240  resmgmhm2b  45242  mgmhmco  45243  mgmhmima  45244  snlindsntorlem  45699  1arymaptf  45875  ipolubdm  46161  ipoglbdm  46164  aacllem  46391