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  760  ad5ant24  761  ad5ant25  762  3adant1  1131  3ad2antl3  1188  ralcom2  3377  vtocl2d  3562  sbc2iegf  3865  sbcralt  3872  pofun  5610  poinxp  5766  xpdifid  6188  sossfld  6206  preddowncl  6353  tz7.7  6410  onfr  6423  ssimaex  6994  eqfnun  7057  fndmdif  7062  dffo4  7123  fompt  7138  fcompt  7153  fconst2g  7223  f1cofveqaeq  7278  2f1fvneq  7280  isores3  7355  fvmptopabOLD  7488  limsssuc  7871  el2mpocl  8111  1stconst  8125  2ndconst  8126  curry1  8129  curry2  8132  poseq  8183  soseq  8184  extmptsuppeq  8213  suppss  8219  suppss2  8225  onnseq  8384  oe0  8560  oesuclem  8563  oecl  8575  oaordi  8584  oawordri  8588  omordi  8604  omword2  8612  omlimcl  8616  odi  8617  omass  8618  oeoe  8637  nnaordi  8656  oaabs  8686  omsmolem  8695  eceqoveq  8862  mapsnd  8926  dom2lem  9032  sbthlem9  9131  rexdif1en  9198  php3OLD  9261  onomeneqOLD  9266  isinf  9296  isinfOLD  9297  frfi  9321  fiint  9366  fiintOLD  9367  fodomfib  9369  fodomfibOLD  9371  fofinf1o  9372  marypha1lem  9473  ordiso2  9555  unwdomg  9624  xpwdomg  9625  frr1  9799  ac5num  10076  cff1  10298  cfcoflem  10312  infpssrlem4  10346  isf32lem9  10401  isf34lem7  10419  fin1a2lem13  10452  fin1a2s  10454  hsmexlem4  10469  axdc2lem  10488  zorn2lem6  10541  axpowndlem2  10638  inttsk  10814  tskuni  10823  nqereu  10969  prcdnq  11033  addclprlem2  11057  ltexpri  11083  prlem936  11087  reclem2pr  11088  axsup  11336  add4  11482  ltleadd  11746  lt2mul2div  12146  nn2ge  12293  zextle  12691  fnn0ind  12717  xrlttr  13182  ifle  13239  xnn0lem1lt  13286  xaddass  13291  xmulasslem3  13328  xlemul1a  13330  xadddilem  13336  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  supxrunb2  13362  ixxin  13404  difreicc  13524  iccsplit  13525  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzaddel  13598  fzadd2  13599  fzrev  13627  modadd1  13948  modmul1  13965  fsuppmapnn0fiub  14032  mulexp  14142  expadd  14145  expmul  14148  expnbnd  14271  bccl  14361  hashdom  14418  prsshashgt1  14449  hashfacen  14493  brfi1uzind  14547  wrdnval  14583  swrdccat3blem  14777  revccat  14804  2shfti  15119  rexico  15392  cau3lem  15393  subcn2  15631  caucvgb  15716  iseraltlem1  15718  sumss  15760  fsumsplitsn  15780  incexclem  15872  supcvg  15892  mertenslem2  15921  fprodn0  16015  fprodsplitsn  16025  fprodle  16032  eftlcl  16143  reeftlcl  16144  rpnnen2lem6  16255  dvdsext  16358  3dvds  16368  sqoddm1div8z  16391  gcdcllem3  16538  dvdsexpim  16592  bezoutr1  16606  seq1st  16608  dvdslcm  16635  lcmeq0  16637  lcmcl  16638  lcmneg  16640  lcmdvds  16645  coprmgcdb  16686  dvdsprime  16724  pc2dvds  16917  prmpwdvds  16942  unbenlem  16946  infpnlem1  16948  1arith  16965  vdwmc2  17017  ramcl  17067  mrcuni  17664  isacs1i  17700  acsfn  17702  funcpropd  17947  curfcl  18277  curf2ndf  18292  resmgmhm  18724  resmgmhm2b  18726  mgmhmco  18727  mgmhmima  18728  resmhm  18833  resmhm2b  18835  mhmco  18836  pwsdiagmhm  18844  gsumwsubmcl  18850  gsumwspan  18859  pwmnd  18950  dfgrp2  18980  subgint  19168  ghmmhmb  19245  resghm  19250  cntzmhm  19359  symgextf1lem  19438  f1omvdconj  19464  dfod2  19582  gexdvds  19602  subgpgp  19615  sylow1lem3  19618  frgpnabllem1  19891  dprdfeq0  20042  rhmimasubrnglem  20565  cntzsubrng  20567  cntzsubr  20606  isdrng2  20743  islmodd  20864  lsslss  20959  reslmhm2b  21053  rngqiprngimfo  21311  psgnfix1  21616  psgndif  21620  copsgndif  21621  ocvocv  21689  frlmsslsp  21816  frlmlbs  21817  psrbaglefi  21946  psrdi  21985  psrass23l  21987  psrass23  21989  psdmul  22170  mptcoe1fsupp  22217  psropprmul  22239  ply1coe  22302  rhmcomulmpl  22386  mamudi  22407  mamudir  22408  mat1dimelbas  22477  scmatmulcl  22524  scmatfo  22536  mulmarep1gsum2  22580  mdetunilem7  22624  mdetunilem9  22626  gsummatr01lem3  22663  smadiadetlem3  22674  cpmadugsumlemF  22882  leordtval  23221  cnpnei  23272  cnco  23274  cnss1  23284  cmpsub  23408  hauscmplem  23414  dissnlocfin  23537  ptbasid  23583  tx2cn  23618  upxp  23631  txindis  23642  xkoptsub  23662  xkopt  23663  trfbas2  23851  filconn  23891  trfil2  23895  filssufilg  23919  ufileu  23927  fixufil  23930  ufilen  23938  rnelfmlem  23960  flimclsi  23986  hauspwpwf1  23995  fclsopn  24022  fclsfnflim  24035  fclscmpi  24037  alexsubALTlem4  24058  ptcmplem5  24064  tgpmulg  24101  subgtgp  24113  tgpt0  24127  tsmsxplem2  24162  metss  24521  metustfbas  24570  dscopn  24586  xrsmopn  24834  cncfss  24925  icoopnst  24969  iccpnfcnv  24975  icccvx  24981  evth  24991  phtpycc  25023  pcohtpylem  25052  lmmbrf  25296  fgcfil  25305  caucfil  25317  cfilres  25330  bcth3  25365  cmscsscms  25407  ovolfioo  25502  ovolficc  25503  voliunlem3  25587  volcn  25641  mbflimsup  25701  mbfi1fseqlem5  25754  itg2seq  25777  bddiblnc  25877  dvnff  25959  dvnadd  25965  cpnord  25971  c1liplem1  26035  plypf1  26251  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeidlem  26276  dgrle  26282  dgrnznn  26286  plycjlem  26316  elqaalem3  26363  ulmcaulem  26437  ulmcau  26438  psergf  26455  psercn2  26466  psercn2OLD  26467  efopn  26700  abscxpbnd  26796  leibpi  26985  isppw2  27158  muinv  27236  bposlem3  27330  gausslemma2dlem4  27413  pntrmax  27608  pntpbnd1  27630  qabvexp  27670  madebday  27938  mulsrid  28139  peano5n0s  28324  zs12bday  28424  eqeelen  28919  colinearalglem4  28924  axcgrid  28931  axsegconlem1  28932  axsegconlem3  28934  ax5seglem1  28943  ax5seglem2  28944  ax5seglem9  28952  axcontlem2  28980  cusgrfilem2  29474  vtxdgfisf  29494  usgr2pthlem  29783  uspgrn2crct  29828  crctcshwlkn0  29841  wwlksnext  29913  wwlksnextproplem3  29931  eupth2lem3lem4  30250  frgr3vlem1  30292  frgr3vlem2  30293  3vfriswmgrlem  30296  frgrwopreglem5  30340  numclwwlk3lem2  30403  grpoidinvlem3  30525  grpoidinv  30527  grpoideu  30528  nmoub3i  30792  nmlno0lem  30812  nmlnoubi  30815  ipasslem3  30852  ipblnfi  30874  hvaddsub4  31097  his35  31107  shsel3  31334  chj4  31554  spansncol  31587  chscllem2  31657  5oalem2  31674  3oalem2  31682  hoaddcl  31777  adjsym  31852  cnvadj  31911  hhcno  31923  hhcnf  31924  nmopub2tALT  31928  unoplin  31939  counop  31940  nmfnleub2  31945  hmoplin  31961  brafnmul  31970  nmlnop0iALT  32014  nmopun  32033  nmophmi  32050  riesz3i  32081  riesz1  32084  cnlnadjlem2  32087  cnlnadjlem6  32091  adjmul  32111  adjadd  32112  bra11  32127  cnvbraval  32129  kbass5  32139  kbass6  32140  leop2  32143  leopadd  32151  leopmuli  32152  leoptri  32155  leopnmid  32157  nmopleid  32158  pj3si  32226  hstel2  32238  cvcon3  32303  dmdmd  32319  dmdbr5  32327  mdsl0  32329  mdslmd1lem1  32344  mdslmd1lem2  32345  mdslmd3i  32351  superpos  32373  chirredlem2  32410  chirredlem3  32411  mdsymlem3  32424  mdsymlem5  32426  mdsymlem6  32427  sumdmdlem  32437  cdjreui  32451  cdj1i  32452  cdj3i  32460  foresf1o  32523  2ndimaxp  32656  abfmpel  32665  fcomptf  32668  fcnvgreu  32683  fdifsuppconst  32698  xrge0infss  32764  xnn0gt0  32773  cycpm2tr  33139  elrgspnlem2  33247  elrgspnlem3  33248  intlidl  33448  rhmpreimaprmidl  33479  lssdimle  33658  mdetpmtr1  33822  cmpcref  33849  xrge0iifcnv  33932  zrhcntr  33980  esumcst  34064  hasheuni  34086  esum2dlem  34093  esum2d  34094  sigaclcu2  34121  insiga  34138  unelldsys  34159  measres  34223  measdivcst  34225  volfiniune  34231  ddemeas  34237  sgn3da  34544  actfunsnf1o  34619  fnrelpredd  35103  fineqvac  35111  sconnpi1  35244  cvmsss2  35279  satfv1lem  35367  fmlaomn0  35395  gonarlem  35399  mrsubco  35526  dfon2lem6  35789  hfext  36184  elicc3  36318  fnessref  36358  bj-ismooredr2  37111  pibt2  37418  fin2solem  37613  fin2so  37614  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem2  37629  poimirlem14  37641  poimirlem25  37652  poimirlem26  37653  poimirlem29  37656  poimirlem30  37657  broucube  37661  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  ex-ovoliunnfl  37670  mbfresfi  37673  cnambfre  37675  itg2addnclem  37678  itg2addnclem2  37679  itg2addnc  37681  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  indexdom  37741  filbcmb  37747  fdc  37752  incsequz  37755  metf1o  37762  caures  37767  bndss  37793  ismtycnv  37809  heiborlem1  37818  rrncmslem  37839  isdrngo2  37965  rngoisocnv  37988  unichnidl  38038  erimeq2  38679  ax12eq  38942  ax12el  38943  lshpset2N  39120  pmapglb2N  39773  pmapglb2xN  39774  pclfinN  39902  polval2N  39908  cdleme31fv2  40395  cdleme32fvcl  40442  cdleme48gfv  40539  tendoicl  40798  tendoipl  40799  diaglbN  41057  dochkr1  41480  dochkr1OLDN  41481  sumcubes  42347  expeq1d  42359  zaddcomlem  42481  zmulcomlem  42485  fiabv  42546  rhmcomulpsr  42561  evlsvvval  42573  selvcllem5  42592  evlselv  42597  fsuppind  42600  fsuppssind  42603  mhpind  42604  nacsfix  42723  eq0rabdioph  42787  diophren  42824  rencldnfilem  42831  pell1234qrdich  42872  jm2.24  42975  jm2.26lem3  43013  wepwsolem  43054  pwssplit4  43101  isnumbasgrplem3  43117  onexoegt  43256  onov0suclim  43287  cantnfresb  43337  omcl2  43346  ofoaid1  43371  ofoaid2  43372  grumnudlem  44304  cvgdvgrat  44332  ofsubid  44343  bcc0  44359  binomcxplemnn0  44368  uzwo4  45058  fiiuncl  45070  iunincfi  45099  nsstr  45100  rexanuz3  45101  iinssiin  45134  disjrnmpt2  45193  disjinfi  45197  choicefi  45205  fsneq  45211  difmap  45212  iunmapsn  45222  axccdom  45227  axccd  45234  rnmptlb  45250  rnmptbd2lem  45255  ssfiunibd  45321  supxrgelem  45348  suplesup  45350  xrlexaddrp  45363  xralrple2  45365  infxrunb2  45379  xralrple3  45385  xrralrecnnle  45394  xrralrecnnge  45401  supxrunb3  45410  unb2ltle  45426  rexabslelem  45429  supminfrnmpt  45456  infxrpnf  45457  supminfxr  45475  supminfxr2  45480  xrpnf  45496  pimxrneun  45499  cvgcaule  45502  iooiinicc  45555  ressioosup  45568  iooiinioc  45569  ressiooinf  45570  fsumsupp0  45593  divcnvg  45642  limcrecl  45644  sumnnodd  45645  islpcn  45654  lptre2pt  45655  limcresiooub  45657  limcresioolb  45658  limclner  45666  fnlimfvre  45689  allbutfifvre  45690  climinf3  45731  limsupmnflem  45735  limsupre3uzlem  45750  limsupreuzmpt  45754  climuzlem  45758  climisp  45761  climrescn  45763  climxrrelem  45764  climxrre  45765  climlimsupcex  45784  liminflelimsuplem  45790  limsupgtlem  45792  liminfvalxr  45798  liminfreuzlem  45817  liminfltlem  45819  liminflimsupclim  45822  xlimpnfxnegmnf  45829  liminflbuz2  45830  liminflimsupxrre  45832  cnrefiisplem  45844  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  xlimmnfmpt  45858  xlimpnfmpt  45859  climxlim2lem  45860  dfxlim2v  45862  xlimliminflimsup  45877  cncfuni  45901  icccncfext  45902  cncficcgt0  45903  cncfiooicclem1  45908  cncfiooiccre  45910  dvasinbx  45935  dvdsn1add  45954  dvnmul  45958  dvmptfprodlem  45959  dvnprodlem1  45961  dvnprodlem3  45963  iblspltprt  45988  itgioocnicc  45992  itgspltprt  45994  ismbl3  46001  stirlinglem5  46093  dirker2re  46107  dirkerper  46111  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem12  46134  fourierdlem15  46137  fourierdlem16  46138  fourierdlem20  46142  fourierdlem21  46143  fourierdlem22  46144  fourierdlem39  46161  fourierdlem40  46162  fourierdlem41  46163  fourierdlem42  46164  fourierdlem46  46167  fourierdlem49  46170  fourierdlem50  46171  fourierdlem57  46178  fourierdlem58  46179  fourierdlem59  46180  fourierdlem64  46185  fourierdlem65  46186  fourierdlem66  46187  fourierdlem68  46189  fourierdlem70  46191  fourierdlem71  46192  fourierdlem73  46194  fourierdlem78  46199  fourierdlem79  46200  fourierdlem80  46201  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem87  46208  fourierdlem93  46214  fourierdlem95  46216  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  sqwvfoura  46243  fourierswlem  46245  elaa2lem  46248  etransclem13  46262  etransclem23  46272  etransclem24  46273  etransclem32  46281  etransclem38  46287  etransclem46  46295  qndenserrnbllem  46309  rrxsnicc  46315  ioorrnopnlem  46319  prsal  46333  intsal  46345  salexct  46349  dfsalgen2  46356  issalnnd  46360  sge0rnre  46379  sge0val  46381  sge0z  46390  sge0revalmpt  46393  sge0tsms  46395  sge0pr  46409  sge0resplit  46421  sge0split  46424  sge0splitmpt  46426  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0fodjrnlem  46431  sge0iunmpt  46433  sge0rpcpnf  46436  sge0ltfirpmpt2  46441  sge0isum  46442  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0pnffsumgt  46457  sge0gtfsumgt  46458  sge0seq  46461  sge0reuz  46462  nnfoctbdjlem  46470  nnfoctbdj  46471  meadjun  46477  meadjiunlem  46480  voliunsge0lem  46487  meaiuninc3v  46499  omeiunltfirp  46534  carageniuncllem2  46537  caratheodorylem1  46541  caratheodorylem2  46542  caratheodory  46543  isomenndlem  46545  isomennd  46546  hoicvr  46563  volicorescl  46568  ovnsubaddlem2  46586  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem2  46617  hspdifhsp  46631  hoiqssbllem2  46638  hoiqssbllem3  46639  hspmbllem2  46642  ovnsubadd2lem  46660  ovolval4lem1  46664  vonvolmbl  46676  vonioo  46697  vonicc  46700  pimrecltpos  46723  issmfle  46760  smflimlem1  46786  smflimlem2  46787  smflimlem6  46791  smfresal  46803  smfrec  46804  smfmullem4  46809  smfpimcc  46823  smflimmpt  46825  smfsuplem1  46826  smfsuplem3  46828  smfsupmpt  46830  smfsupxr  46831  smfinflem  46832  smfinfmpt  46834  smflimsuplem4  46838  smflimsuplem5  46839  smflimsupmpt  46844  smfliminfmpt  46847  fsupdm  46857  finfdm  46861  smonoord  47358  lswn0  47431  poprelb  47511  fmtnoprmfac1  47552  fmtnofac2lem  47555  sbgoldbst  47765  isgrim  47868  gpgedgvtx0  48019  snlindsntorlem  48387  1arymaptf  48562  ipolubdm  48876  ipoglbdm  48879  aacllem  49320