Theorem adantll 715

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 581	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  728  ad2ant2l  747  ad2ant2lr  749  ad5ant23  760  ad5ant24  761  ad5ant25  762  3adant1  1131  3ad2antl3  1189  ralcom2  3340  vtocl2d  3508  sbc2iegf  3804  sbcralt  3811  pofun  5550  poinxp  5705  xpdifid  6126  sossfld  6144  preddowncl  6290  tz7.7  6343  onfr  6356  ssimaex  6919  eqfnun  6983  fndmdif  6988  dffo4  7049  fompt  7064  fcompt  7080  fconst2g  7151  f1cofveqaeq  7205  isores3  7283  limsssuc  7794  el2mpocl  8029  1stconst  8043  2ndconst  8044  curry1  8047  curry2  8050  poseq  8101  soseq  8102  extmptsuppeq  8131  suppss  8137  suppss2  8143  onnseq  8277  oe0  8450  oesuclem  8453  oecl  8465  oaordi  8474  oawordri  8478  omordi  8494  omword2  8502  omlimcl  8506  odi  8507  omass  8508  oeoe  8528  nnaordi  8547  oaabs  8577  omsmolem  8586  eceqoveq  8762  mapsnd  8827  dom2lem  8932  sbthlem9  9026  rexdif1en  9088  isinf  9168  frfi  9188  fiint  9230  fodomfib  9232  fodomfibOLD  9234  fofinf1o  9235  marypha1lem  9339  ordiso2  9423  unwdomg  9492  xpwdomg  9493  frr1  9674  ac5num  9949  cff1  10171  cfcoflem  10185  infpssrlem4  10219  isf32lem9  10274  isf34lem7  10292  fin1a2lem13  10325  fin1a2s  10327  hsmexlem4  10342  axdc2lem  10361  zorn2lem6  10414  axpowndlem2  10512  inttsk  10688  tskuni  10697  nqereu  10843  prcdnq  10907  addclprlem2  10931  ltexpri  10957  prlem936  10961  reclem2pr  10962  axsup  11212  add4  11358  ltleadd  11624  lt2mul2div  12025  nn2ge  12195  zextle  12593  fnn0ind  12619  xrlttr  13082  ifle  13140  xnn0lem1lt  13187  xaddass  13192  xmulasslem3  13229  xlemul1a  13231  xadddilem  13237  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  ixxin  13306  difreicc  13428  iccsplit  13429  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  fzaddel  13503  fzadd2  13504  fzrev  13532  modadd1  13858  modmul1  13877  fsuppmapnn0fiub  13944  mulexp  14054  expadd  14057  expmul  14060  expnbnd  14185  bccl  14275  hashdom  14332  prsshashgt1  14363  hashfacen  14407  brfi1uzind  14461  wrdnval  14498  swrdccat3blem  14692  revccat  14719  2shfti  15033  rexico  15307  cau3lem  15308  subcn2  15548  caucvgb  15633  iseraltlem1  15635  sumss  15677  fsumsplitsn  15697  incexclem  15792  supcvg  15812  mertenslem2  15841  fprodn0  15935  fprodsplitsn  15945  fprodle  15952  eftlcl  16065  reeftlcl  16066  rpnnen2lem6  16177  dvdsext  16281  3dvds  16291  sqoddm1div8z  16314  gcdcllem3  16461  dvdsexpim  16515  bezoutr1  16529  seq1st  16531  dvdslcm  16558  lcmeq0  16560  lcmcl  16561  lcmneg  16563  lcmdvds  16568  coprmgcdb  16609  dvdsprime  16647  pc2dvds  16841  prmpwdvds  16866  unbenlem  16870  infpnlem1  16872  1arith  16889  vdwmc2  16941  ramcl  16991  mrcuni  17578  isacs1i  17614  acsfn  17616  funcpropd  17860  curfcl  18189  curf2ndf  18204  resmgmhm  18670  resmgmhm2b  18672  mgmhmco  18673  mgmhmima  18674  resmhm  18779  resmhm2b  18781  mhmco  18782  pwsdiagmhm  18790  gsumwsubmcl  18796  gsumwspan  18805  pwmnd  18899  dfgrp2  18929  subgint  19117  ghmmhmb  19193  resghm  19198  cntzmhm  19307  symgextf1lem  19386  f1omvdconj  19412  dfod2  19530  gexdvds  19550  subgpgp  19563  sylow1lem3  19566  frgpnabllem1  19839  dprdfeq0  19990  rhmimasubrnglem  20533  cntzsubrng  20535  cntzsubr  20574  isdrng2  20711  islmodd  20852  lsslss  20947  reslmhm2b  21041  rngqiprngimfo  21291  psgnfix1  21588  psgndif  21592  copsgndif  21593  ocvocv  21661  frlmsslsp  21786  frlmlbs  21787  psrbaglefi  21916  psrdi  21953  psrass23l  21955  psrass23  21957  evlsvvval  22081  psdmul  22142  mptcoe1fsupp  22189  psropprmul  22211  ply1coe  22273  rhmcomulmpl  22357  mamudi  22378  mamudir  22379  mat1dimelbas  22446  scmatmulcl  22493  scmatfo  22505  mulmarep1gsum2  22549  mdetunilem7  22593  mdetunilem9  22595  gsummatr01lem3  22632  smadiadetlem3  22643  cpmadugsumlemF  22851  leordtval  23188  cnpnei  23239  cnco  23241  cnss1  23251  cmpsub  23375  hauscmplem  23381  dissnlocfin  23504  ptbasid  23550  tx2cn  23585  upxp  23598  txindis  23609  xkoptsub  23629  xkopt  23630  trfbas2  23818  filconn  23858  trfil2  23862  filssufilg  23886  ufileu  23894  fixufil  23897  ufilen  23905  rnelfmlem  23927  flimclsi  23953  hauspwpwf1  23962  fclsopn  23989  fclsfnflim  24002  fclscmpi  24004  alexsubALTlem4  24025  ptcmplem5  24031  tgpmulg  24068  subgtgp  24080  tgpt0  24094  tsmsxplem2  24129  metss  24483  metustfbas  24532  dscopn  24548  xrsmopn  24788  cncfss  24876  icoopnst  24916  iccpnfcnv  24921  icccvx  24927  evth  24936  phtpycc  24968  pcohtpylem  24996  lmmbrf  25239  fgcfil  25248  caucfil  25260  cfilres  25273  bcth3  25308  cmscsscms  25350  ovolfioo  25444  ovolficc  25445  voliunlem3  25529  volcn  25583  mbflimsup  25643  mbfi1fseqlem5  25696  itg2seq  25719  bddiblnc  25819  dvnff  25900  dvnadd  25906  cpnord  25912  c1liplem1  25973  plypf1  26187  plyaddlem1  26188  plymullem1  26189  coeeulem  26199  coeidlem  26212  dgrle  26218  dgrnznn  26222  plycjlem  26251  elqaalem3  26298  ulmcaulem  26372  ulmcau  26373  psergf  26390  psercn2  26401  efopn  26635  abscxpbnd  26730  leibpi  26919  isppw2  27092  muinv  27170  bposlem3  27263  gausslemma2dlem4  27346  pntrmax  27541  pntpbnd1  27563  qabvexp  27603  madebday  27906  mulsrid  28119  bdayons  28282  peano5n0s  28325  bdaypw2n0bndlem  28469  bdayfinlem  28492  eqeelen  28987  colinearalglem4  28992  axcgrid  28999  axsegconlem1  29000  axsegconlem3  29002  ax5seglem1  29011  ax5seglem2  29012  ax5seglem9  29020  axcontlem2  29048  cusgrfilem2  29540  vtxdgfisf  29560  usgr2pthlem  29846  uspgrn2crct  29891  crctcshwlkn0  29904  wwlksnext  29976  wwlksnextproplem3  29994  eupth2lem3lem4  30316  frgr3vlem1  30358  frgr3vlem2  30359  3vfriswmgrlem  30362  frgrwopreglem5  30406  numclwwlk3lem2  30469  grpoidinvlem3  30592  grpoidinv  30594  grpoideu  30595  nmoub3i  30859  nmlno0lem  30879  nmlnoubi  30882  ipasslem3  30919  ipblnfi  30941  hvaddsub4  31164  his35  31174  shsel3  31401  chj4  31621  spansncol  31654  chscllem2  31724  5oalem2  31741  3oalem2  31749  hoaddcl  31844  adjsym  31919  cnvadj  31978  hhcno  31990  hhcnf  31991  nmopub2tALT  31995  unoplin  32006  counop  32007  nmfnleub2  32012  hmoplin  32028  brafnmul  32037  nmlnop0iALT  32081  nmopun  32100  nmophmi  32117  riesz3i  32148  riesz1  32151  cnlnadjlem2  32154  cnlnadjlem6  32158  adjmul  32178  adjadd  32179  bra11  32194  cnvbraval  32196  kbass5  32206  kbass6  32207  leop2  32210  leopadd  32218  leopmuli  32219  leoptri  32222  leopnmid  32224  nmopleid  32225  pj3si  32293  hstel2  32305  cvcon3  32370  dmdmd  32386  dmdbr5  32394  mdsl0  32396  mdslmd1lem1  32411  mdslmd1lem2  32412  mdslmd3i  32418  superpos  32440  chirredlem2  32477  chirredlem3  32478  mdsymlem3  32491  mdsymlem5  32493  mdsymlem6  32494  sumdmdlem  32504  cdjreui  32518  cdj1i  32519  cdj3i  32527  foresf1o  32589  2ndimaxp  32734  abfmpel  32743  fcomptf  32746  fcnvgreu  32760  fdifsuppconst  32777  xrge0infss  32848  xnn0gt0  32857  sgn3da  32922  cycpm2tr  33195  elrgspnlem2  33319  elrgspnlem3  33320  intlidl  33495  rhmpreimaprmidl  33526  mplvrpmga  33704  psrmonmul  33709  esplyfval0  33723  vieta  33739  lssdimle  33767  mdetpmtr1  33983  cmpcref  34010  xrge0iifcnv  34093  zrhcntr  34139  esumcst  34223  hasheuni  34245  esum2dlem  34252  esum2d  34253  sigaclcu2  34280  insiga  34297  unelldsys  34318  measres  34382  measdivcst  34384  volfiniune  34390  ddemeas  34396  actfunsnf1o  34764  fnrelpredd  35250  fineqvac  35276  fineqvnttrclselem1  35281  sconnpi1  35437  cvmsss2  35472  satfv1lem  35560  fmlaomn0  35588  gonarlem  35592  mrsubco  35719  dfon2lem6  35984  hfext  36381  elicc3  36515  fnessref  36555  bj-ismooredr2  37438  pibt2  37747  fin2solem  37941  fin2so  37942  lindsenlbs  37950  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem2  37957  poimirlem14  37969  poimirlem25  37980  poimirlem26  37981  poimirlem29  37984  poimirlem30  37985  broucube  37989  heicant  37990  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ex-ovoliunnfl  37998  mbfresfi  38001  cnambfre  38003  itg2addnclem  38006  itg2addnclem2  38007  itg2addnc  38009  ftc1anclem3  38030  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  indexdom  38069  filbcmb  38075  fdc  38080  incsequz  38083  metf1o  38090  caures  38095  bndss  38121  ismtycnv  38137  heiborlem1  38146  rrncmslem  38167  isdrngo2  38293  rngoisocnv  38316  unichnidl  38366  erimeq2  39098  ax12eq  39401  ax12el  39402  lshpset2N  39579  pmapglb2N  40231  pmapglb2xN  40232  pclfinN  40360  polval2N  40366  cdleme31fv2  40853  cdleme32fvcl  40900  cdleme48gfv  40997  tendoicl  41256  tendoipl  41257  diaglbN  41515  dochkr1  41938  dochkr1OLDN  41939  sumcubes  42759  expeq1d  42770  zaddcomlem  42922  zmulcomlem  42926  fiabv  42995  rhmcomulpsr  43008  selvcllem5  43029  evlselv  43034  fsuppind  43037  fsuppssind  43040  mhpind  43041  nacsfix  43158  eq0rabdioph  43222  diophren  43259  rencldnfilem  43266  pell1234qrdich  43307  jm2.24  43409  jm2.26lem3  43447  wepwsolem  43488  pwssplit4  43535  isnumbasgrplem3  43551  onexoegt  43690  onov0suclim  43720  cantnfresb  43770  omcl2  43779  ofoaid1  43804  ofoaid2  43805  grumnudlem  44730  cvgdvgrat  44758  ofsubid  44769  bcc0  44785  binomcxplemnn0  44794  uzwo4  45502  fiiuncl  45514  iunincfi  45542  nsstr  45543  rexanuz3  45544  iinssiin  45577  disjrnmpt2  45636  disjinfi  45640  choicefi  45647  fsneq  45653  difmap  45654  iunmapsn  45664  axccdom  45669  axccd  45676  rnmptlb  45690  rnmptbd2lem  45695  ssfiunibd  45760  supxrgelem  45785  suplesup  45787  xrlexaddrp  45800  xralrple2  45802  infxrunb2  45815  xralrple3  45821  xrralrecnnle  45830  xrralrecnnge  45837  supxrunb3  45846  unb2ltle  45861  rexabslelem  45864  supminfrnmpt  45891  infxrpnf  45892  supminfxr  45910  supminfxr2  45915  xrpnf  45931  pimxrneun  45934  cvgcaule  45937  iooiinicc  45990  ressioosup  46003  iooiinioc  46004  ressiooinf  46005  fsumsupp0  46026  divcnvg  46075  limcrecl  46077  sumnnodd  46078  islpcn  46085  lptre2pt  46086  limcresiooub  46088  limcresioolb  46089  limclner  46097  fnlimfvre  46120  allbutfifvre  46121  climinf3  46162  limsupmnflem  46166  limsupre3uzlem  46181  limsupreuzmpt  46185  climuzlem  46189  climisp  46192  climrescn  46194  climxrrelem  46195  climxrre  46196  climlimsupcex  46215  liminflelimsuplem  46221  limsupgtlem  46223  liminfvalxr  46229  liminfreuzlem  46248  liminfltlem  46250  liminflimsupclim  46253  xlimpnfxnegmnf  46260  liminflbuz2  46261  liminflimsupxrre  46263  cnrefiisplem  46275  xlimmnfvlem2  46279  xlimmnfv  46280  xlimpnfvlem2  46283  xlimpnfv  46284  xlimmnfmpt  46289  xlimpnfmpt  46290  climxlim2lem  46291  dfxlim2v  46293  xlimliminflimsup  46308  cncfuni  46332  icccncfext  46333  cncficcgt0  46334  cncfiooicclem1  46339  cncfiooiccre  46341  dvasinbx  46366  dvdsn1add  46385  dvnmul  46389  dvmptfprodlem  46390  dvnprodlem1  46392  dvnprodlem3  46394  iblspltprt  46419  itgioocnicc  46423  itgspltprt  46425  ismbl3  46432  stirlinglem5  46524  dirker2re  46538  dirkerper  46542  dirkertrigeq  46547  dirkercncflem2  46550  fourierdlem12  46565  fourierdlem15  46568  fourierdlem16  46569  fourierdlem20  46573  fourierdlem21  46574  fourierdlem22  46575  fourierdlem39  46592  fourierdlem40  46593  fourierdlem41  46594  fourierdlem42  46595  fourierdlem46  46598  fourierdlem49  46601  fourierdlem50  46602  fourierdlem57  46609  fourierdlem58  46610  fourierdlem59  46611  fourierdlem64  46616  fourierdlem65  46617  fourierdlem66  46618  fourierdlem68  46620  fourierdlem70  46622  fourierdlem71  46623  fourierdlem73  46625  fourierdlem78  46630  fourierdlem79  46631  fourierdlem80  46632  fourierdlem81  46633  fourierdlem82  46634  fourierdlem83  46635  fourierdlem87  46639  fourierdlem93  46645  fourierdlem95  46647  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  sqwvfoura  46674  fourierswlem  46676  elaa2lem  46679  etransclem13  46693  etransclem23  46703  etransclem24  46704  etransclem32  46712  etransclem38  46718  etransclem46  46726  qndenserrnbllem  46740  rrxsnicc  46746  ioorrnopnlem  46750  prsal  46764  intsal  46776  salexct  46780  dfsalgen2  46787  issalnnd  46791  sge0rnre  46810  sge0val  46812  sge0z  46821  sge0revalmpt  46824  sge0tsms  46826  sge0pr  46840  sge0resplit  46852  sge0split  46855  sge0splitmpt  46857  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0fodjrnlem  46862  sge0iunmpt  46864  sge0rpcpnf  46867  sge0ltfirpmpt2  46872  sge0isum  46873  sge0xaddlem1  46879  sge0xaddlem2  46880  sge0pnffsumgt  46888  sge0gtfsumgt  46889  sge0seq  46892  sge0reuz  46893  nnfoctbdjlem  46901  nnfoctbdj  46902  meadjun  46908  meadjiunlem  46911  voliunsge0lem  46918  meaiuninc3v  46930  omeiunltfirp  46965  carageniuncllem2  46968  caratheodorylem1  46972  caratheodorylem2  46973  caratheodory  46974  isomenndlem  46976  isomennd  46977  hoicvr  46994  volicorescl  46999  ovnsubaddlem2  47017  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvle  47046  ovnhoilem2  47048  hspdifhsp  47062  hoiqssbllem2  47069  hoiqssbllem3  47070  hspmbllem2  47073  ovnsubadd2lem  47091  ovolval4lem1  47095  vonvolmbl  47107  vonioo  47128  vonicc  47131  pimrecltpos  47154  issmfle  47191  smflimlem1  47217  smflimlem2  47218  smflimlem6  47222  smfresal  47234  smfrec  47235  smfmullem4  47240  smfpimcc  47254  smflimmpt  47256  smfsuplem1  47257  smfsuplem3  47259  smfsupmpt  47261  smfsupxr  47262  smfinflem  47263  smfinfmpt  47265  smflimsuplem4  47269  smflimsuplem5  47270  smflimsupmpt  47275  smfliminfmpt  47278  fsupdm  47288  finfdm  47292  smonoord  47837  lswn0  47916  poprelb  47996  fmtnoprmfac1  48040  fmtnofac2lem  48043  sbgoldbst  48266  isgrim  48370  gpgedgvtx0  48549  snlindsntorlem  48958  1arymaptf  49129  ipolubdm  49474  ipoglbdm  49477  setc1onsubc  50089  aacllem  50288