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  3351  vtocl2d  3528  sbc2iegf  3828  sbcralt  3835  pofun  5564  poinxp  5719  xpdifid  6141  sossfld  6159  preddowncl  6305  tz7.7  6358  onfr  6371  ssimaex  6946  eqfnun  7009  fndmdif  7014  dffo4  7075  fompt  7090  fcompt  7105  fconst2g  7177  f1cofveqaeq  7232  isores3  7310  fvmptopabOLD  7444  limsssuc  7826  el2mpocl  8065  1stconst  8079  2ndconst  8080  curry1  8083  curry2  8086  poseq  8137  soseq  8138  extmptsuppeq  8167  suppss  8173  suppss2  8179  onnseq  8313  oe0  8486  oesuclem  8489  oecl  8501  oaordi  8510  oawordri  8514  omordi  8530  omword2  8538  omlimcl  8542  odi  8543  omass  8544  oeoe  8563  nnaordi  8582  oaabs  8612  omsmolem  8621  eceqoveq  8795  mapsnd  8859  dom2lem  8963  sbthlem9  9059  rexdif1en  9122  isinf  9207  isinfOLD  9208  frfi  9232  fiint  9277  fiintOLD  9278  fodomfib  9280  fodomfibOLD  9282  fofinf1o  9283  marypha1lem  9384  ordiso2  9468  unwdomg  9537  xpwdomg  9538  frr1  9712  ac5num  9989  cff1  10211  cfcoflem  10225  infpssrlem4  10259  isf32lem9  10314  isf34lem7  10332  fin1a2lem13  10365  fin1a2s  10367  hsmexlem4  10382  axdc2lem  10401  zorn2lem6  10454  axpowndlem2  10551  inttsk  10727  tskuni  10736  nqereu  10882  prcdnq  10946  addclprlem2  10970  ltexpri  10996  prlem936  11000  reclem2pr  11001  axsup  11249  add4  11395  ltleadd  11661  lt2mul2div  12061  nn2ge  12213  zextle  12607  fnn0ind  12633  xrlttr  13100  ifle  13157  xnn0lem1lt  13204  xaddass  13209  xmulasslem3  13246  xlemul1a  13248  xadddilem  13254  xrsupsslem  13267  xrinfmsslem  13268  supxrunb1  13279  supxrunb2  13280  ixxin  13323  difreicc  13445  iccsplit  13446  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzaddel  13519  fzadd2  13520  fzrev  13548  modadd1  13870  modmul1  13889  fsuppmapnn0fiub  13956  mulexp  14066  expadd  14069  expmul  14072  expnbnd  14197  bccl  14287  hashdom  14344  prsshashgt1  14375  hashfacen  14419  brfi1uzind  14473  wrdnval  14510  swrdccat3blem  14704  revccat  14731  2shfti  15046  rexico  15320  cau3lem  15321  subcn2  15561  caucvgb  15646  iseraltlem1  15648  sumss  15690  fsumsplitsn  15710  incexclem  15802  supcvg  15822  mertenslem2  15851  fprodn0  15945  fprodsplitsn  15955  fprodle  15962  eftlcl  16075  reeftlcl  16076  rpnnen2lem6  16187  dvdsext  16291  3dvds  16301  sqoddm1div8z  16324  gcdcllem3  16471  dvdsexpim  16525  bezoutr1  16539  seq1st  16541  dvdslcm  16568  lcmeq0  16570  lcmcl  16571  lcmneg  16573  lcmdvds  16578  coprmgcdb  16619  dvdsprime  16657  pc2dvds  16850  prmpwdvds  16875  unbenlem  16879  infpnlem1  16881  1arith  16898  vdwmc2  16950  ramcl  17000  mrcuni  17582  isacs1i  17618  acsfn  17620  funcpropd  17864  curfcl  18193  curf2ndf  18208  resmgmhm  18638  resmgmhm2b  18640  mgmhmco  18641  mgmhmima  18642  resmhm  18747  resmhm2b  18749  mhmco  18750  pwsdiagmhm  18758  gsumwsubmcl  18764  gsumwspan  18773  pwmnd  18864  dfgrp2  18894  subgint  19082  ghmmhmb  19159  resghm  19164  cntzmhm  19273  symgextf1lem  19350  f1omvdconj  19376  dfod2  19494  gexdvds  19514  subgpgp  19527  sylow1lem3  19530  frgpnabllem1  19803  dprdfeq0  19954  rhmimasubrnglem  20474  cntzsubrng  20476  cntzsubr  20515  isdrng2  20652  islmodd  20772  lsslss  20867  reslmhm2b  20961  rngqiprngimfo  21211  psgnfix1  21507  psgndif  21511  copsgndif  21512  ocvocv  21580  frlmsslsp  21705  frlmlbs  21706  psrbaglefi  21835  psrdi  21874  psrass23l  21876  psrass23  21878  psdmul  22053  mptcoe1fsupp  22100  psropprmul  22122  ply1coe  22185  rhmcomulmpl  22269  mamudi  22290  mamudir  22291  mat1dimelbas  22358  scmatmulcl  22405  scmatfo  22417  mulmarep1gsum2  22461  mdetunilem7  22505  mdetunilem9  22507  gsummatr01lem3  22544  smadiadetlem3  22555  cpmadugsumlemF  22763  leordtval  23100  cnpnei  23151  cnco  23153  cnss1  23163  cmpsub  23287  hauscmplem  23293  dissnlocfin  23416  ptbasid  23462  tx2cn  23497  upxp  23510  txindis  23521  xkoptsub  23541  xkopt  23542  trfbas2  23730  filconn  23770  trfil2  23774  filssufilg  23798  ufileu  23806  fixufil  23809  ufilen  23817  rnelfmlem  23839  flimclsi  23865  hauspwpwf1  23874  fclsopn  23901  fclsfnflim  23914  fclscmpi  23916  alexsubALTlem4  23937  ptcmplem5  23943  tgpmulg  23980  subgtgp  23992  tgpt0  24006  tsmsxplem2  24041  metss  24396  metustfbas  24445  dscopn  24461  xrsmopn  24701  cncfss  24792  icoopnst  24836  iccpnfcnv  24842  icccvx  24848  evth  24858  phtpycc  24890  pcohtpylem  24919  lmmbrf  25162  fgcfil  25171  caucfil  25183  cfilres  25196  bcth3  25231  cmscsscms  25273  ovolfioo  25368  ovolficc  25369  voliunlem3  25453  volcn  25507  mbflimsup  25567  mbfi1fseqlem5  25620  itg2seq  25643  bddiblnc  25743  dvnff  25825  dvnadd  25831  cpnord  25837  c1liplem1  25901  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  dgrle  26148  dgrnznn  26152  plycjlem  26182  elqaalem3  26229  ulmcaulem  26303  ulmcau  26304  psergf  26321  psercn2  26332  psercn2OLD  26333  efopn  26567  abscxpbnd  26663  leibpi  26852  isppw2  27025  muinv  27103  bposlem3  27197  gausslemma2dlem4  27280  pntrmax  27475  pntpbnd1  27497  qabvexp  27537  madebday  27811  mulsrid  28016  bdayon  28173  peano5n0s  28212  zs12bday  28343  eqeelen  28831  colinearalglem4  28836  axcgrid  28843  axsegconlem1  28844  axsegconlem3  28846  ax5seglem1  28855  ax5seglem2  28856  ax5seglem9  28864  axcontlem2  28892  cusgrfilem2  29384  vtxdgfisf  29404  usgr2pthlem  29693  uspgrn2crct  29738  crctcshwlkn0  29751  wwlksnext  29823  wwlksnextproplem3  29841  eupth2lem3lem4  30160  frgr3vlem1  30202  frgr3vlem2  30203  3vfriswmgrlem  30206  frgrwopreglem5  30250  numclwwlk3lem2  30313  grpoidinvlem3  30435  grpoidinv  30437  grpoideu  30438  nmoub3i  30702  nmlno0lem  30722  nmlnoubi  30725  ipasslem3  30762  ipblnfi  30784  hvaddsub4  31007  his35  31017  shsel3  31244  chj4  31464  spansncol  31497  chscllem2  31567  5oalem2  31584  3oalem2  31592  hoaddcl  31687  adjsym  31762  cnvadj  31821  hhcno  31833  hhcnf  31834  nmopub2tALT  31838  unoplin  31849  counop  31850  nmfnleub2  31855  hmoplin  31871  brafnmul  31880  nmlnop0iALT  31924  nmopun  31943  nmophmi  31960  riesz3i  31991  riesz1  31994  cnlnadjlem2  31997  cnlnadjlem6  32001  adjmul  32021  adjadd  32022  bra11  32037  cnvbraval  32039  kbass5  32049  kbass6  32050  leop2  32053  leopadd  32061  leopmuli  32062  leoptri  32065  leopnmid  32067  nmopleid  32068  pj3si  32136  hstel2  32148  cvcon3  32213  dmdmd  32229  dmdbr5  32237  mdsl0  32239  mdslmd1lem1  32254  mdslmd1lem2  32255  mdslmd3i  32261  superpos  32283  chirredlem2  32320  chirredlem3  32321  mdsymlem3  32334  mdsymlem5  32336  mdsymlem6  32337  sumdmdlem  32347  cdjreui  32361  cdj1i  32362  cdj3i  32370  foresf1o  32433  2ndimaxp  32570  abfmpel  32579  fcomptf  32582  fcnvgreu  32597  fdifsuppconst  32612  xrge0infss  32683  xnn0gt0  32692  sgn3da  32759  cycpm2tr  33076  elrgspnlem2  33194  elrgspnlem3  33195  intlidl  33391  rhmpreimaprmidl  33422  lssdimle  33603  mdetpmtr1  33813  cmpcref  33840  xrge0iifcnv  33923  zrhcntr  33969  esumcst  34053  hasheuni  34075  esum2dlem  34082  esum2d  34083  sigaclcu2  34110  insiga  34127  unelldsys  34148  measres  34212  measdivcst  34214  volfiniune  34220  ddemeas  34226  actfunsnf1o  34595  fnrelpredd  35079  fineqvac  35087  sconnpi1  35226  cvmsss2  35261  satfv1lem  35349  fmlaomn0  35377  gonarlem  35381  mrsubco  35508  dfon2lem6  35776  hfext  36171  elicc3  36305  fnessref  36345  bj-ismooredr2  37098  pibt2  37405  fin2solem  37600  fin2so  37601  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem2  37616  poimirlem14  37628  poimirlem25  37639  poimirlem26  37640  poimirlem29  37643  poimirlem30  37644  broucube  37648  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ex-ovoliunnfl  37657  mbfresfi  37660  cnambfre  37662  itg2addnclem  37665  itg2addnclem2  37666  itg2addnc  37668  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  indexdom  37728  filbcmb  37734  fdc  37739  incsequz  37742  metf1o  37749  caures  37754  bndss  37780  ismtycnv  37796  heiborlem1  37805  rrncmslem  37826  isdrngo2  37952  rngoisocnv  37975  unichnidl  38025  erimeq2  38670  ax12eq  38934  ax12el  38935  lshpset2N  39112  pmapglb2N  39765  pmapglb2xN  39766  pclfinN  39894  polval2N  39900  cdleme31fv2  40387  cdleme32fvcl  40434  cdleme48gfv  40531  tendoicl  40790  tendoipl  40791  diaglbN  41049  dochkr1  41472  dochkr1OLDN  41473  sumcubes  42301  expeq1d  42312  zaddcomlem  42451  zmulcomlem  42455  fiabv  42524  rhmcomulpsr  42539  evlsvvval  42551  selvcllem5  42570  evlselv  42575  fsuppind  42578  fsuppssind  42581  mhpind  42582  nacsfix  42700  eq0rabdioph  42764  diophren  42801  rencldnfilem  42808  pell1234qrdich  42849  jm2.24  42952  jm2.26lem3  42990  wepwsolem  43031  pwssplit4  43078  isnumbasgrplem3  43094  onexoegt  43233  onov0suclim  43263  cantnfresb  43313  omcl2  43322  ofoaid1  43347  ofoaid2  43348  grumnudlem  44274  cvgdvgrat  44302  ofsubid  44313  bcc0  44329  binomcxplemnn0  44338  uzwo4  45047  fiiuncl  45059  iunincfi  45088  nsstr  45089  rexanuz3  45090  iinssiin  45123  disjrnmpt2  45182  disjinfi  45186  choicefi  45194  fsneq  45200  difmap  45201  iunmapsn  45211  axccdom  45216  axccd  45223  rnmptlb  45237  rnmptbd2lem  45242  ssfiunibd  45307  supxrgelem  45333  suplesup  45335  xrlexaddrp  45348  xralrple2  45350  infxrunb2  45364  xralrple3  45370  xrralrecnnle  45379  xrralrecnnge  45386  supxrunb3  45395  unb2ltle  45411  rexabslelem  45414  supminfrnmpt  45441  infxrpnf  45442  supminfxr  45460  supminfxr2  45465  xrpnf  45481  pimxrneun  45484  cvgcaule  45487  iooiinicc  45540  ressioosup  45553  iooiinioc  45554  ressiooinf  45555  fsumsupp0  45576  divcnvg  45625  limcrecl  45627  sumnnodd  45628  islpcn  45637  lptre2pt  45638  limcresiooub  45640  limcresioolb  45641  limclner  45649  fnlimfvre  45672  allbutfifvre  45673  climinf3  45714  limsupmnflem  45718  limsupre3uzlem  45733  limsupreuzmpt  45737  climuzlem  45741  climisp  45744  climrescn  45746  climxrrelem  45747  climxrre  45748  climlimsupcex  45767  liminflelimsuplem  45773  limsupgtlem  45775  liminfvalxr  45781  liminfreuzlem  45800  liminfltlem  45802  liminflimsupclim  45805  xlimpnfxnegmnf  45812  liminflbuz2  45813  liminflimsupxrre  45815  cnrefiisplem  45827  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem2  45835  xlimpnfv  45836  xlimmnfmpt  45841  xlimpnfmpt  45842  climxlim2lem  45843  dfxlim2v  45845  xlimliminflimsup  45860  cncfuni  45884  icccncfext  45885  cncficcgt0  45886  cncfiooicclem1  45891  cncfiooiccre  45893  dvasinbx  45918  dvdsn1add  45937  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem1  45944  dvnprodlem3  45946  iblspltprt  45971  itgioocnicc  45975  itgspltprt  45977  ismbl3  45984  stirlinglem5  46076  dirker2re  46090  dirkerper  46094  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem12  46117  fourierdlem15  46120  fourierdlem16  46121  fourierdlem20  46125  fourierdlem21  46126  fourierdlem22  46127  fourierdlem39  46144  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem46  46150  fourierdlem49  46153  fourierdlem50  46154  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem64  46168  fourierdlem65  46169  fourierdlem66  46170  fourierdlem68  46172  fourierdlem70  46174  fourierdlem71  46175  fourierdlem73  46177  fourierdlem78  46182  fourierdlem79  46183  fourierdlem80  46184  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem87  46191  fourierdlem93  46197  fourierdlem95  46199  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  sqwvfoura  46226  fourierswlem  46228  elaa2lem  46231  etransclem13  46245  etransclem23  46255  etransclem24  46256  etransclem32  46264  etransclem38  46270  etransclem46  46278  qndenserrnbllem  46292  rrxsnicc  46298  ioorrnopnlem  46302  prsal  46316  intsal  46328  salexct  46332  dfsalgen2  46339  issalnnd  46343  sge0rnre  46362  sge0val  46364  sge0z  46373  sge0revalmpt  46376  sge0tsms  46378  sge0pr  46392  sge0resplit  46404  sge0split  46407  sge0splitmpt  46409  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0fodjrnlem  46414  sge0iunmpt  46416  sge0rpcpnf  46419  sge0ltfirpmpt2  46424  sge0isum  46425  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0seq  46444  sge0reuz  46445  nnfoctbdjlem  46453  nnfoctbdj  46454  meadjun  46460  meadjiunlem  46463  voliunsge0lem  46470  meaiuninc3v  46482  omeiunltfirp  46517  carageniuncllem2  46520  caratheodorylem1  46524  caratheodorylem2  46525  caratheodory  46526  isomenndlem  46528  isomennd  46529  hoicvr  46546  volicorescl  46551  ovnsubaddlem2  46569  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvle  46598  ovnhoilem2  46600  hspdifhsp  46614  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem2  46625  ovnsubadd2lem  46643  ovolval4lem1  46647  vonvolmbl  46659  vonioo  46680  vonicc  46683  pimrecltpos  46706  issmfle  46743  smflimlem1  46769  smflimlem2  46770  smflimlem6  46774  smfresal  46786  smfrec  46787  smfmullem4  46792  smfpimcc  46806  smflimmpt  46808  smfsuplem1  46809  smfsuplem3  46811  smfsupmpt  46813  smfsupxr  46814  smfinflem  46815  smfinfmpt  46817  smflimsuplem4  46821  smflimsuplem5  46822  smflimsupmpt  46827  smfliminfmpt  46830  fsupdm  46840  finfdm  46844  smonoord  47372  lswn0  47445  poprelb  47525  fmtnoprmfac1  47566  fmtnofac2lem  47569  sbgoldbst  47779  isgrim  47882  gpgedgvtx0  48052  snlindsntorlem  48459  1arymaptf  48630  ipolubdm  48975  ipoglbdm  48978  setc1onsubc  49591  aacllem  49790