Theorem adantll 726

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad2antlr  739  ad2ant2l  758  ad2ant2lr  760  ad5ant23  771  ad5ant24  772  ad5ant25  773  3adant1  1148  3ad2antl3  1206  ralcom2  3366  vtocl2d  3528  sbc2iegf  3818  sbcralt  3825  pofun  5587  poinxp  5742  xpdifid  6165  xpdifcnvepel  6166  sossfld  6184  preddowncl  6333  tz7.7  6386  onfr  6400  ssimaex  6966  fsneq  7030  eqfnun  7032  fndmdif  7037  dffo4  7098  fompt  7113  fcompt  7129  fconst2g  7201  f1cofveqaeq  7255  isores3  7333  limsssuc  7842  el2mpocl  8077  1stconst  8091  2ndconst  8092  curry1  8095  curry2  8098  poseq  8150  soseq  8151  extmptsuppeq  8180  suppss  8186  suppss2  8192  onnseq  8327  oe0  8503  oesuclem  8506  oecl  8518  oaordi  8527  oawordri  8531  omordi  8547  omword2  8555  omlimcl  8559  odi  8560  omass  8561  oeoe  8581  nnaordi  8600  oaabs  8630  omsmolem  8639  eceqoveq  8816  mapsnd  8880  dom2lem  8985  sbthlem9  9079  rexdif1en  9141  isinf  9221  frfi  9241  fiint  9282  fodomfib  9284  fofinf1o  9285  marypha1lem  9389  ordiso2  9473  unwdomg  9542  xpwdomg  9543  frr1  9727  ac5num  10016  cff1  10237  cfcoflem  10251  infpssrlem4  10285  isf32lem9  10340  isf34lem7  10358  fin1a2lem13  10391  fin1a2s  10393  hsmexlem4  10408  axdc2lem  10427  zorn2lem6  10480  axpowndlem2  10578  inttsk  10754  tskuni  10763  nqereu  10909  prcdnq  10973  addclprlem2  10997  ltexpri  11023  prlem936  11027  reclem2pr  11028  axsup  11280  add4  11426  ltleadd  11692  lt2mul2div  12088  nn2ge  12258  zextle  12664  fnn0ind  12690  xrlttr  13160  ifle  13218  xnn0lem1lt  13265  xaddass  13270  xmulasslem3  13307  xlemul1a  13309  xadddilem  13315  xrsupsslem  13328  xrinfmsslem  13329  supxrunb1  13340  supxrunb2  13341  ixxin  13384  difreicc  13506  iccsplit  13507  iccshftr  13508  iccshftl  13510  iccdil  13512  icccntr  13514  fzaddel  13582  fzadd2  13583  fzrev  13611  modadd1  13937  modmul1  13956  fsuppmapnn0fiub  14023  mulexp  14133  expadd  14136  expmul  14139  expnbnd  14264  bccl  14354  hashdom  14411  prsshashgt1  14443  hashfacen  14487  brfi1uzind  14541  wrdnval  14578  swrdccat3blem  14772  revccat  14799  2shfti  15113  sgn3da  15134  rexico  15401  cau3lem  15402  subcn2  15642  caucvgb  15727  iseraltlem1  15729  sumss  15771  fsumsplitsn  15791  incexclem  15886  supcvg  15906  mertenslem2  15935  fprodn0  16029  fprodsplitsn  16039  fprodle  16046  eftlcl  16158  reeftlcl  16159  rpnnen2lem6  16270  dvdsext  16374  3dvds  16384  sqoddm1div8z  16407  gcdcllem3  16554  dvdsexpim  16608  bezoutr1  16622  seq1st  16624  dvdslcm  16651  lcmeq0  16653  lcmcl  16654  lcmneg  16656  lcmdvds  16661  coprmgcdb  16702  dvdsprime  16740  pc2dvds  16934  prmpwdvds  16959  unbenlem  16963  infpnlem1  16965  1arith  16982  vdwmc2  17034  ramcl  17084  mrcuni  17672  isacs1i  17708  acsfn  17710  funcpropd  17954  curfcl  18283  curf2ndf  18298  resmgmhm  18764  resmgmhm2b  18766  mgmhmco  18767  mgmhmima  18768  resmhm  18874  resmhm2b  18876  mhmco  18877  pwsdiagmhm  18885  gsumwsubmcl  18891  gsumwspan  18900  pwmnd  18994  dfgrp2  19024  subgint  19212  ghmmhmb  19292  resghm  19297  cntzmhm  19406  symgextf1lem  19485  f1omvdconj  19511  dfod2  19629  gexdvds  19649  subgpgp  19662  sylow1lem3  19665  frgpnabllem1  19938  dprdfeq0  20089  rhmimasubrnglem  20664  cntzsubrng  20666  cntzsubr  20705  isdrng2  20843  isdrng3lem1  20851  islmodd  20987  lsslss  21082  reslmhm2b  21175  rngqiprngimfo  21441  rhmpreimaprmidl  21479  psgnfix1  21748  psgndif  21752  copsgndif  21753  ocvocv  21821  frlmsslsp  21946  frlmlbs  21947  psrbaglefi  22076  psrdi  22114  psrass23l  22116  psrass23  22118  evlsvvval  22244  rhmcomulmpl  22275  selvcllem5  22290  psdmul  22329  mptcoe1fsupp  22375  psropprmul  22397  ply1coe  22458  mamudi  22560  mamudir  22561  mat1dimelbas  22628  scmatmulcl  22675  scmatfo  22687  mulmarep1gsum2  22731  mdetunilem7  22775  mdetunilem9  22777  gsummatr01lem3  22814  smadiadetlem3  22825  cpmadugsumlemF  23033  leordtval  23370  cnpnei  23421  cnco  23423  cnss1  23433  cmpsub  23557  hauscmplem  23563  dissnlocfin  23686  ptbasid  23732  tx2cn  23767  upxp  23780  txindis  23791  xkoptsub  23811  xkopt  23812  trfbas2  24000  filconn  24040  trfil2  24044  filssufilg  24068  ufileu  24076  fixufil  24079  ufilen  24087  rnelfmlem  24109  flimclsi  24135  hauspwpwf1  24144  fclsopn  24171  fclsfnflim  24184  fclscmpi  24186  alexsubALTlem4  24207  ptcmplem5  24213  tgpmulg  24250  subgtgp  24262  tgpt0  24276  tsmsxplem2  24311  metss  24665  metustfbas  24714  dscopn  24730  xrsmopn  24970  cncfss  25058  icoopnst  25098  iccpnfcnv  25103  icccvx  25109  evth  25118  phtpycc  25150  pcohtpylem  25178  lmmbrf  25421  fgcfil  25430  caucfil  25442  cfilres  25455  bcth3  25490  cmscsscms  25532  ovolfioo  25626  ovolficc  25627  voliunlem3  25711  volcn  25765  mbflimsup  25825  mbfi1fseqlem5  25878  itg2seq  25901  bddiblnc  26001  dvnff  26082  dvnadd  26088  cpnord  26094  c1liplem1  26155  plypf1  26369  plyaddlem1  26370  plymullem1  26371  coeeulem  26381  coeidlem  26394  dgrle  26400  dgrnznn  26404  plycjlem  26433  elqaalem3  26482  ulmcaulem  26557  ulmcau  26558  psergf  26575  psercn2  26586  efopn  26823  abscxpbnd  26918  leibpi  27107  isppw2  27279  muinv  27357  bposlem3  27450  gausslemma2dlem4  27533  pntrmax  27728  pntpbnd1  27750  qabvexp  27790  madebday  28093  mulsrid  28306  bdayons  28469  peano5n0s  28512  bdaypw2n0bndlem  28656  bdayfinlem  28679  eqeelen  29254  colinearalglem4  29259  axcgrid  29266  axsegconlem1  29267  axsegconlem3  29269  ax5seglem1  29278  ax5seglem2  29279  ax5seglem9  29287  axcontlem2  29315  cusgrfilem2  29806  vtxdgfisf  29826  usgr2pthlem  30112  uspgrn2crct  30157  crctcshwlkn0  30170  wwlksnext  30242  wwlksnextproplem3  30260  eupth2lem3lem4  30582  frgr3vlem1  30624  frgr3vlem2  30625  3vfriswmgrlem  30628  frgrwopreglem5  30672  numclwwlk3lem2  30735  grpoidinvlem3  30858  grpoidinv  30860  grpoideu  30861  nmoub3i  31125  nmlno0lem  31145  nmlnoubi  31148  ipasslem3  31185  ipblnfi  31207  hvaddsub4  31430  his35  31440  shsel3  31667  chj4  31887  spansncol  31920  chscllem2  31990  5oalem2  32007  3oalem2  32015  hoaddcl  32110  adjsym  32185  cnvadj  32244  hhcno  32256  hhcnf  32257  nmopub2tALT  32261  unoplin  32272  counop  32273  nmfnleub2  32278  hmoplin  32294  brafnmul  32303  nmlnop0iALT  32347  nmopun  32366  nmophmi  32383  riesz3i  32414  riesz1  32417  cnlnadjlem2  32420  cnlnadjlem6  32424  adjmul  32444  adjadd  32445  bra11  32460  cnvbraval  32462  kbass5  32472  kbass6  32473  leop2  32476  leopadd  32484  leopmuli  32485  leoptri  32488  leopnmid  32490  nmopleid  32491  pj3si  32559  hstel2  32571  cvcon3  32636  dmdmd  32652  dmdbr5  32660  mdsl0  32662  mdslmd1lem1  32677  mdslmd1lem2  32678  mdslmd3i  32684  superpos  32706  chirredlem2  32743  chirredlem3  32744  mdsymlem3  32757  mdsymlem5  32759  mdsymlem6  32760  sumdmdlem  32770  cdjreui  32784  cdj1i  32785  cdj3i  32793  foresf1o  32850  2ndimaxp  32991  abfmpel  33000  fcomptf  33003  fcnvgreu  33017  fdifsuppconst  33034  xrge0infss  33105  xnn0gt0  33114  cycpm2tr  33439  elrgspnlem2  33563  elrgspnlem3  33564  intlidl  33728  mplvrpmga  33935  psrmonmul  33940  esplyfval0  33954  vieta  33970  lssdimle  33998  mdetpmtr1  34213  cmpcref  34240  xrge0iifcnv  34323  zrhcntr  34369  esumcst  34453  hasheuni  34475  esum2dlem  34482  esum2d  34483  sigaclcu2  34510  insiga  34527  unelldsys  34548  measres  34612  measdivcst  34614  volfiniune  34620  ddemeas  34626  actfunsnf1o  34991  fnrelpredd  35482  fineqvac  35529  fineqvnttrclselem1  35534  sconnpi1  35731  cvmsss2  35766  satfv1lem  35854  fmlaomn0  35882  gonarlem  35886  mrsubco  36013  dfon2lem6  36278  hfext  36675  elicc3  36828  fnessref  36868  bj-ismooredr2  37752  pibt2  38063  fin2solem  38257  fin2so  38258  lindsenlbs  38266  matunitlindflem1  38267  matunitlindflem2  38268  poimirlem2  38273  poimirlem14  38285  poimirlem25  38296  poimirlem26  38297  poimirlem29  38300  poimirlem30  38301  broucube  38305  heicant  38306  mblfinlem2  38309  mblfinlem3  38310  mblfinlem4  38311  ex-ovoliunnfl  38314  mbfresfi  38317  cnambfre  38319  itg2addnclem  38322  itg2addnclem2  38323  itg2addnc  38325  ftc1anclem3  38346  ftc1anclem4  38347  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  ftc1anclem8  38351  ftc1anc  38352  indexdom  38385  filbcmb  38391  fdc  38396  incsequz  38399  metf1o  38406  caures  38411  bndss  38437  ismtycnv  38453  heiborlem1  38462  rrncmslem  38483  isdrngo2  38609  rngoisocnv  38632  unichnidl  38682  erimeq2  39412  ax12eq  39715  ax12el  39716  lshpset2N  39893  pmapglb2N  40545  pmapglb2xN  40546  pclfinN  40674  polval2N  40680  cdleme31fv2  41167  cdleme32fvcl  41214  cdleme48gfv  41311  tendoicl  41570  tendoipl  41571  diaglbN  41829  dochkr1  42252  dochkr1OLDN  42253  sumcubes  43074  expeq1d  43085  zaddcomlem  43237  zmulcomlem  43241  fiabv  43304  rhmcomulpsr  43314  evlselv  43321  fsuppind  43322  fsuppssind  43325  mhpind  43326  nacsfix  43443  eq0rabdioph  43507  diophren  43540  rencldnfilem  43547  pell1234qrdich  43588  jm2.24  43690  jm2.26lem3  43728  wepwsolem  43769  pwssplit4  43816  isnumbasgrplem3  43832  onexoegt  43971  onov0suclim  44001  cantnfresb  44051  omcl2  44060  ofoaid1  44085  ofoaid2  44086  grumnudlem  44995  cvgdvgrat  45023  ofsubid  45034  bcc0  45050  binomcxplemnn0  45059  uzwo4  45773  fiiuncl  45785  iunincfi  45812  nsstr  45813  rexanuz3  45814  iinssiin  45847  disjrnmpt2  45906  disjinfi  45910  choicefi  45917  difmap  45923  iunmapsn  45933  axccdom  45938  axccd  45944  rnmptlb  45958  rnmptbd2lem  45963  ssfiunibd  46028  supxrgelem  46053  suplesup  46055  xrlexaddrp  46068  xralrple2  46070  infxrunb2  46083  xralrple3  46089  xrralrecnnle  46098  xrralrecnnge  46105  supxrunb3  46114  unb2ltle  46129  rexabslelem  46132  supminfrnmpt  46159  infxrpnf  46160  supminfxr  46178  supminfxr2  46183  xrpnf  46199  pimxrneun  46202  cvgcaule  46205  iooiinicc  46258  ressioosup  46271  iooiinioc  46272  ressiooinf  46273  fsumsupp0  46294  divcnvg  46343  limcrecl  46345  sumnnodd  46346  islpcn  46353  lptre2pt  46354  limcresiooub  46356  limcresioolb  46357  limclner  46365  fnlimfvre  46388  allbutfifvre  46389  climinf3  46430  limsupmnflem  46434  limsupre3uzlem  46449  limsupreuzmpt  46453  climuzlem  46457  climisp  46460  climrescn  46462  climxrrelem  46463  climxrre  46464  climlimsupcex  46483  liminflelimsuplem  46489  limsupgtlem  46491  liminfvalxr  46497  liminfreuzlem  46516  liminfltlem  46518  liminflimsupclim  46521  xlimpnfxnegmnf  46528  liminflbuz2  46529  liminflimsupxrre  46531  cnrefiisplem  46543  xlimmnfvlem2  46547  xlimmnfv  46548  xlimpnfvlem2  46551  xlimpnfv  46552  xlimmnfmpt  46557  xlimpnfmpt  46558  climxlim2lem  46559  dfxlim2v  46561  xlimliminflimsup  46576  cncfuni  46600  icccncfext  46601  cncficcgt0  46602  cncfiooicclem1  46607  cncfiooiccre  46609  dvasinbx  46634  dvdsn1add  46653  dvnmul  46657  dvmptfprodlem  46658  dvnprodlem1  46660  dvnprodlem3  46662  iblspltprt  46687  itgioocnicc  46691  itgspltprt  46693  ismbl3  46700  stirlinglem5  46792  dirker2re  46806  dirkerper  46810  dirkertrigeq  46815  dirkercncflem2  46818  fourierdlem12  46833  fourierdlem15  46836  fourierdlem16  46837  fourierdlem20  46841  fourierdlem21  46842  fourierdlem22  46843  fourierdlem39  46860  fourierdlem40  46861  fourierdlem41  46862  fourierdlem42  46863  fourierdlem46  46866  fourierdlem49  46869  fourierdlem50  46870  fourierdlem57  46877  fourierdlem58  46878  fourierdlem59  46879  fourierdlem64  46884  fourierdlem65  46885  fourierdlem66  46886  fourierdlem68  46888  fourierdlem70  46890  fourierdlem71  46891  fourierdlem73  46893  fourierdlem78  46898  fourierdlem79  46899  fourierdlem80  46900  fourierdlem81  46901  fourierdlem82  46902  fourierdlem83  46903  fourierdlem87  46907  fourierdlem93  46913  fourierdlem95  46915  fourierdlem101  46921  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem112  46932  sqwvfoura  46942  fourierswlem  46944  elaa2lem  46947  etransclem13  46961  etransclem23  46971  etransclem24  46972  etransclem32  46980  etransclem38  46986  etransclem46  46994  qndenserrnbllem  47008  rrxsnicc  47014  ioorrnopnlem  47018  prsal  47032  intsal  47044  salexct  47048  dfsalgen2  47055  issalnnd  47059  sge0rnre  47078  sge0val  47080  sge0z  47089  sge0revalmpt  47092  sge0tsms  47094  sge0pr  47108  sge0resplit  47120  sge0split  47123  sge0splitmpt  47125  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0fodjrnlem  47130  sge0iunmpt  47132  sge0rpcpnf  47135  sge0ltfirpmpt2  47140  sge0isum  47141  sge0xaddlem1  47147  sge0xaddlem2  47148  sge0pnffsumgt  47156  sge0gtfsumgt  47157  sge0seq  47160  sge0reuz  47161  nnfoctbdjlem  47169  nnfoctbdj  47170  meadjun  47176  meadjiunlem  47179  voliunsge0lem  47186  meaiuninc3v  47198  omeiunltfirp  47233  carageniuncllem2  47236  caratheodorylem1  47240  caratheodorylem2  47241  caratheodory  47242  isomenndlem  47244  isomennd  47245  hoicvr  47262  volicorescl  47267  ovnsubaddlem2  47285  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvle  47314  ovnhoilem2  47316  hspdifhsp  47330  hoiqssbllem2  47337  hoiqssbllem3  47338  hspmbllem2  47341  ovnsubadd2lem  47359  ovolval4lem1  47363  vonvolmbl  47375  vonioo  47396  vonicc  47399  pimrecltpos  47422  issmfle  47459  smflimlem1  47485  smflimlem2  47486  smflimlem6  47490  smfresal  47502  smfrec  47503  smfmullem4  47508  smfpimcc  47522  smflimmpt  47524  smfsuplem1  47525  smfsuplem3  47527  smfsupmpt  47529  smfsupxr  47530  smfinflem  47531  smfinfmpt  47533  smflimsuplem4  47537  smflimsuplem5  47538  smflimsupmpt  47543  smfliminfmpt  47546  fsupdm  47556  finfdm  47560  smonoord  48114  lswn0  48193  poprelb  48273  fmtnoprmfac1  48317  fmtnofac2lem  48320  sbgoldbst  48543  isgrim  48647  gpgedgvtx0  48826  snlindsntorlem  49250  1arymaptf  49421  ipolubdm  49765  ipoglbdm  49768  setc1onsubc  50380  aacllem  50621