Theorem adantll 701

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  ad2antlr  714  ad2ant2l  733  ad2ant2lr  735  ad4ant23  740  ad4ant24  741  ad5ant23  747  ad5ant24  748  ad5ant25  749  3adant1  1110  3ad2antl3  1167  ralcom2  3304  reu6  3631  sbc2iegf  3754  sbcralt  3760  pofun  5344  poinxp  5483  xpdifid  5867  sossfld  5885  predpo  6006  preddowncl  6015  tz7.7  6057  onfr  6070  ssimaex  6578  fndmdif  6639  dffo4  6694  fcompt  6720  fconst2g  6794  f1cofveqaeq  6843  2f1fvneq  6845  isores3  6913  fvmptopab  7030  limsssuc  7383  el2mpocl  7591  1stconst  7605  2ndconst  7606  curry1  7609  curry2  7612  extmptsuppeq  7659  suppss  7665  suppssov1  7667  suppss2  7669  onnseq  7787  oe0  7951  oesuclem  7954  oecl  7966  oaordi  7975  oawordri  7979  omordi  7995  omword2  8003  omlimcl  8007  odi  8008  omass  8009  oeoe  8028  nnaordi  8047  oaabs  8073  omsmolem  8082  eceqoveq  8204  mapsnd  8250  dom2lem  8348  sbthlem9  8433  php3  8501  onomeneq  8505  isinf  8528  frfi  8560  fiint  8592  fodomfib  8595  fofinf1o  8596  marypha1lem  8694  ordiso2  8776  unwdomg  8845  xpwdomg  8846  ac5num  9258  cff1  9480  cfcoflem  9494  infpssrlem4  9528  isf32lem9  9583  isf34lem7  9601  fin1a2lem13  9634  fin1a2s  9636  hsmexlem4  9651  axdc2lem  9670  zorn2lem6  9723  axpowndlem2  9820  inttsk  9996  tskuni  10005  nqereu  10151  prcdnq  10215  addclprlem2  10239  ltexpri  10265  prlem936  10269  reclem2pr  10270  axsup  10518  add4  10662  ltleadd  10926  lt2mul2div  11321  nn2ge  11470  zextle  11871  fnn0ind  11897  xrlttr  12353  ifle  12410  xaddass  12461  xmulasslem3  12498  xlemul1a  12500  xadddilem  12506  xrsupsslem  12519  xrinfmsslem  12520  supxrunb1  12531  supxrunb2  12532  ixxin  12574  difreicc  12689  iccsplit  12690  iccshftr  12691  iccshftl  12693  iccdil  12695  icccntr  12697  fzaddel  12760  fzadd2  12761  fzrev  12789  modadd1  13094  modmul1  13110  fsuppmapnn0fiub  13177  mulexp  13286  expadd  13289  expmul  13292  expnbnd  13411  bccl  13500  hashdom  13556  prsshashgt1  13587  hashfacen  13628  brfi1uzind  13670  wrdnval  13710  swrdccat3blem  13947  revccat  13988  2shfti  14303  rexico  14577  cau3lem  14578  subcn2  14815  caucvgb  14900  iseraltlem1  14902  sumss  14944  fsumsplitsn  14963  incexclem  15054  supcvg  15074  mertenslem2  15104  fprodn0  15196  fprodsplitsn  15206  fprodle  15213  eftlcl  15323  reeftlcl  15324  rpnnen2lem6  15435  dvdsext  15534  3dvds  15543  sqoddm1div8z  15566  gcdcllem3  15713  bezoutr1  15772  seq1st  15774  dvdslcm  15801  lcmeq0  15803  lcmcl  15804  lcmneg  15806  lcmdvds  15811  coprmgcdb  15852  dvdsprime  15890  pc2dvds  16074  prmpwdvds  16099  unbenlem  16103  infpnlem1  16105  1arith  16122  vdwmc2  16174  ramcl  16224  mrcuni  16753  isacs1i  16789  acsfn  16791  funcpropd  17031  curfcl  17343  curf2ndf  17358  resmhm  17830  resmhm2b  17832  mhmco  17833  mhmima  17834  pwsdiagmhm  17840  gsumwsubmcl  17846  gsumwspan  17855  dfgrp2  17919  grpissubg  18086  subgint  18090  ghmmhmb  18143  resghm  18148  cntzmhm  18243  symgextf1lem  18312  f1omvdconj  18338  dfod2  18455  gexdvds  18473  subgpgp  18486  sylow1lem3  18489  frgpnabllem1  18752  dprdfeq0  18897  isdrng2  19238  cntzsubr  19293  islmodd  19365  lsslss  19458  reslmhm2b  19551  psrbaglefi  19869  mptcoe1fsupp  20089  ply1coe  20170  psgnfix1  20447  psgndif  20451  copsgndif  20452  ocvocv  20520  frlmsslsp  20645  frlmlbs  20646  mamudi  20719  mamudir  20720  mat1dimelbas  20787  scmatmulcl  20834  scmatfo  20846  mulmarep1gsum2  20890  mdetunilem7  20934  mdetunilem9  20936  gsummatr01lem3  20973  smadiadetlem3  20984  cpmadugsumlemF  21191  leordtval  21528  cnpnei  21579  cnco  21581  cnss1  21591  cmpsub  21715  hauscmplem  21721  dissnlocfin  21844  ptbasid  21890  tx2cn  21925  upxp  21938  txindis  21949  xkoptsub  21969  xkopt  21970  trfbas2  22158  filconn  22198  trfil2  22202  filssufilg  22226  ufileu  22234  fixufil  22237  ufilen  22245  rnelfmlem  22267  flimclsi  22293  hauspwpwf1  22302  fclsopn  22329  fclsfnflim  22342  fclscmpi  22344  alexsubALTlem4  22365  ptcmplem5  22371  tgpmulg  22408  subgtgp  22420  tgpt0  22433  tsmsxplem2  22468  metss  22824  metustfbas  22873  dscopn  22889  xrsmopn  23126  cncfss  23213  icoopnst  23249  iccpnfcnv  23254  icccvx  23260  evth  23269  phtpycc  23301  pcohtpylem  23329  lmmbrf  23571  fgcfil  23580  caucfil  23592  cfilres  23605  bcth3  23640  cmscsscms  23682  ovolfioo  23774  ovolficc  23775  voliunlem3  23859  volcn  23913  mbflimsup  23973  mbfi1fseqlem5  24026  itg2seq  24049  dvnff  24226  dvnadd  24232  cpnord  24238  c1liplem1  24299  plypf1  24508  plyaddlem1  24509  plymullem1  24510  coeeulem  24520  coeidlem  24533  dgrle  24539  dgrnznn  24543  plycjlem  24572  elqaalem3  24616  ulmcaulem  24688  ulmcau  24689  psergf  24706  psercn2  24717  efopn  24945  abscxpbnd  25038  leibpi  25225  isppw2  25397  muinv  25475  bposlem3  25567  gausslemma2dlem4  25650  pntrmax  25845  pntpbnd1  25867  qabvexp  25907  eqeelen  26396  colinearalglem4  26401  axcgrid  26408  axsegconlem1  26409  axsegconlem3  26411  ax5seglem1  26420  ax5seglem2  26421  ax5seglem9  26429  axcontlem2  26457  cusgrfilem2  26944  vtxdgfisf  26964  usgr2pthlem  27255  uspgrn2crct  27297  crctcshwlkn0  27310  wwlksnextproplem3  27416  wwlksnextproplem3OLD  27417  eupth2lem3lem4  27764  frgr3vlem1  27810  frgr3vlem2  27811  3vfriswmgrlem  27814  frgrwopreglem5  27858  numclwwlk3lem2  27944  grpoidinvlem3  28063  grpoidinv  28065  grpoideu  28066  nmoub3i  28330  nmlno0lem  28350  nmlnoubi  28353  ipasslem3  28390  ipblnfi  28413  hvaddsub4  28637  his35  28647  shsel3  28876  chj4  29096  spansncol  29129  chscllem2  29199  5oalem2  29216  3oalem2  29224  hoaddcl  29319  adjsym  29394  cnvadj  29453  hhcno  29465  hhcnf  29466  nmopub2tALT  29470  unoplin  29481  counop  29482  nmfnleub2  29487  hmoplin  29503  brafnmul  29512  nmlnop0iALT  29556  nmopun  29575  nmophmi  29592  riesz3i  29623  riesz1  29626  cnlnadjlem2  29629  cnlnadjlem6  29633  adjmul  29653  adjadd  29654  bra11  29669  cnvbraval  29671  kbass5  29681  kbass6  29682  leop2  29685  leopadd  29693  leopmuli  29694  leoptri  29697  leopnmid  29699  nmopleid  29700  pj3si  29768  hstel2  29780  cvcon3  29845  dmdmd  29861  dmdbr5  29869  mdsl0  29871  mdslmd1lem1  29886  mdslmd1lem2  29887  mdslmd3i  29893  superpos  29915  chirredlem2  29952  chirredlem3  29953  mdsymlem3  29966  mdsymlem5  29968  mdsymlem6  29969  sumdmdlem  29979  cdjreui  29993  cdj1i  29994  cdj3i  30002  foresf1o  30047  abfmpel  30165  fcomptf  30168  fcnvgreu  30183  xrge0infss  30239  xnn0gt0  30249  xnn0lem1lt  30250  lssdimle  30635  mdetpmtr1  30730  cmpcref  30758  xrge0iifcnv  30820  esumcst  30966  hasheuni  30988  esum2dlem  30995  esum2d  30996  sigaclcu2  31024  insiga  31041  unelldsys  31062  measres  31126  measdivcst  31129  volfiniune  31134  ddemeas  31140  sgn3da  31445  actfunsnf1o  31523  sconnpi1  32071  cvmsss2  32106  mrsubco  32288  dfon2lem6  32553  dftrpred3g  32593  poseq  32616  soseq  32617  frr1  32665  hfext  33165  elicc3  33186  fnessref  33226  pibt2  34139  fin2solem  34319  fin2so  34320  lindsenlbs  34328  matunitlindflem1  34329  matunitlindflem2  34330  poimirlem2  34335  poimirlem14  34347  poimirlem25  34358  poimirlem26  34359  poimirlem29  34362  poimirlem30  34363  broucube  34367  heicant  34368  mblfinlem2  34371  mblfinlem3  34372  mblfinlem4  34373  ex-ovoliunnfl  34376  mbfresfi  34379  cnambfre  34381  itg2addnclem  34384  itg2addnclem2  34385  itg2addnc  34387  bddiblnc  34403  ftc1anclem3  34410  ftc1anclem4  34411  ftc1anclem5  34412  ftc1anclem6  34413  ftc1anclem7  34414  ftc1anclem8  34415  ftc1anc  34416  eqfnun  34439  indexdom  34451  filbcmb  34457  fdc  34462  incsequz  34465  metf1o  34472  caures  34477  bndss  34506  ismtycnv  34522  heiborlem1  34531  rrncmslem  34552  isdrngo2  34678  rngoisocnv  34701  unichnidl  34751  erim2  35356  ax12eq  35522  ax12el  35523  lshpset2N  35700  pmapglb2N  36352  pmapglb2xN  36353  pclfinN  36481  polval2N  36487  cdleme31fv2  36974  cdleme32fvcl  37021  cdleme48gfv  37118  tendoicl  37377  tendoipl  37378  diaglbN  37636  dochkr1  38059  dochkr1OLDN  38060  dvdsexpim  38613  nacsfix  38704  eq0rabdioph  38769  diophren  38806  rencldnfilem  38813  pell1234qrdich  38854  jm2.24  38956  jm2.26lem3  38994  wepwsolem  39038  pwssplit4  39085  isnumbasgrplem3  39101  grumnudlem  39996  cvgdvgrat  40061  ofsubid  40072  bcc0  40088  binomcxplemnn0  40097  uzwo4  40735  fiiuncl  40747  iunincfi  40782  nsstr  40783  rexanuz3  40785  iinssiin  40818  ralimda  40829  disjrnmpt2  40874  fompt  40878  disjinfi  40879  choicefi  40889  fsneq  40895  difmap  40896  iunmapsn  40906  axccdom  40913  axccd  40922  rnmptlb  40942  rnmptbd2lem  40949  ssfiunibd  41006  supxrgelem  41035  suplesup  41037  xrlexaddrp  41050  xralrple2  41052  infxrunb2  41066  xralrple3  41072  xrralrecnnle  41084  xrralrecnnge  41093  supxrunb3  41103  unb2ltle  41121  rexabslelem  41124  supminfrnmpt  41151  infxrpnf  41153  supminfxr  41172  supminfxr2  41177  xrpnf  41194  iooiinicc  41250  ressioosup  41263  iooiinioc  41264  ressiooinf  41265  fsumsupp0  41291  divcnvg  41340  limcrecl  41342  sumnnodd  41343  islpcn  41352  lptre2pt  41353  limcresiooub  41355  limcresioolb  41356  limclner  41364  fnlimfvre  41387  allbutfifvre  41388  climinf3  41429  limsupmnflem  41433  limsupre3uzlem  41448  limsupreuzmpt  41452  climuzlem  41456  climisp  41459  climrescn  41461  climxrrelem  41462  climxrre  41463  climlimsupcex  41482  liminflelimsuplem  41488  limsupgtlem  41490  liminfvalxr  41496  liminfreuzlem  41515  liminfltlem  41517  liminflimsupclim  41520  xlimpnfxnegmnf  41527  liminflbuz2  41528  liminflimsupxrre  41530  cnrefiisplem  41542  xlimmnfvlem2  41546  xlimmnfv  41547  xlimpnfvlem2  41550  xlimpnfv  41551  xlimmnfmpt  41556  xlimpnfmpt  41557  climxlim2lem  41558  dfxlim2v  41560  xlimliminflimsup  41575  cncfuni  41600  icccncfext  41601  cncficcgt0  41602  cncfiooicclem1  41607  cncfiooiccre  41609  dvasinbx  41636  dvdsn1add  41655  dvnmul  41659  dvmptfprodlem  41660  dvnprodlem1  41662  dvnprodlem3  41664  iblspltprt  41689  itgioocnicc  41693  itgspltprt  41695  ismbl3  41703  stirlinglem5  41795  dirker2re  41809  dirkerper  41813  dirkertrigeq  41818  dirkercncflem2  41821  fourierdlem12  41836  fourierdlem15  41839  fourierdlem16  41840  fourierdlem20  41844  fourierdlem21  41845  fourierdlem22  41846  fourierdlem39  41863  fourierdlem40  41864  fourierdlem41  41865  fourierdlem42  41866  fourierdlem46  41869  fourierdlem49  41872  fourierdlem50  41873  fourierdlem57  41880  fourierdlem58  41881  fourierdlem59  41882  fourierdlem64  41887  fourierdlem65  41888  fourierdlem66  41889  fourierdlem68  41891  fourierdlem70  41893  fourierdlem71  41894  fourierdlem73  41896  fourierdlem78  41901  fourierdlem79  41902  fourierdlem80  41903  fourierdlem81  41904  fourierdlem82  41905  fourierdlem83  41906  fourierdlem87  41910  fourierdlem93  41916  fourierdlem95  41918  fourierdlem101  41924  fourierdlem103  41926  fourierdlem104  41927  fourierdlem111  41934  fourierdlem112  41935  sqwvfoura  41945  fourierswlem  41947  elaa2lem  41950  etransclem13  41964  etransclem23  41974  etransclem24  41975  etransclem32  41983  etransclem38  41989  etransclem46  41997  qndenserrnbllem  42011  rrxsnicc  42017  ioorrnopnlem  42021  prsal  42035  intsal  42045  salexct  42049  dfsalgen2  42056  issalnnd  42060  sge0rnre  42078  sge0val  42080  sge0z  42089  sge0revalmpt  42092  sge0tsms  42094  sge0pr  42108  sge0resplit  42120  sge0split  42123  sge0splitmpt  42125  sge0iunmptlemfi  42127  sge0iunmptlemre  42129  sge0fodjrnlem  42130  sge0iunmpt  42132  sge0rpcpnf  42135  sge0ltfirpmpt2  42140  sge0isum  42141  sge0xaddlem1  42147  sge0xaddlem2  42148  sge0pnffsumgt  42156  sge0gtfsumgt  42157  sge0seq  42160  sge0reuz  42161  nnfoctbdjlem  42169  nnfoctbdj  42170  meadjun  42176  meadjiunlem  42179  voliunsge0lem  42186  meaiuninc3v  42198  omeiunltfirp  42233  carageniuncllem2  42236  caratheodorylem1  42240  caratheodorylem2  42241  caratheodory  42242  isomenndlem  42244  isomennd  42245  hoicvr  42262  volicorescl  42267  ovnsubaddlem2  42285  hoidmvlelem2  42310  hoidmvlelem3  42311  hoidmvle  42314  ovnhoilem2  42316  hspdifhsp  42330  hoiqssbllem2  42337  hoiqssbllem3  42338  hspmbllem2  42341  ovnsubadd2lem  42359  ovolval4lem1  42363  vonvolmbl  42375  vonioo  42396  vonicc  42399  pimrecltpos  42419  issmfle  42454  smflimlem1  42479  smflimlem2  42480  smflimlem6  42484  smfresal  42495  smfrec  42496  smfmullem4  42501  smfpimcc  42514  smflimmpt  42516  smfsuplem1  42517  smfsuplem3  42519  smfsupmpt  42521  smfsupxr  42522  smfinflem  42523  smfinfmpt  42525  smflimsuplem4  42529  smflimsuplem5  42530  smflimsupmpt  42535  smfliminfmpt  42538  smonoord  42938  lswn0  42977  poprelb  43055  fmtnoprmfac1  43096  fmtnofac2lem  43099  sbgoldbst  43312  resmgmhm  43434  resmgmhm2b  43436  mgmhmco  43437  mgmhmima  43438  snlindsntorlem  43893  aacllem  44270