Theorem adantll 727

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2antlr  740  ad2ant2l  759  ad2ant2lr  761  ad5ant23  772  ad5ant24  773  ad5ant25  774  3adant1  1148  3ad2antl3  1206  ralcom2  3362  vtocl2d  3523  sbc2iegf  3813  sbcralt  3819  pofun  5577  poinxp  5733  xpdifid  6161  xpdifcnvepel  6162  sossfld  6180  preddowncl  6338  tz7.7  6391  onfr  6405  ssimaex  6975  fsneq  7039  eqfnun  7041  fndmdif  7046  dffo4  7108  fompt  7123  fcompt  7139  fconst2g  7213  f1cofveqaeq  7265  isores3  7347  limsssuc  7865  el2mpocl  8101  1stconst  8117  2ndconst  8118  curry1  8121  curry2  8124  poseq  8181  soseq  8182  extmptsuppeq  8212  suppss  8218  suppss2  8224  onnseq  8359  oe0  8537  oesuclem  8540  oecl  8552  oaordi  8561  oawordri  8565  omordi  8581  omword2  8589  omlimcl  8593  odi  8594  omass  8595  oeoe  8615  nnaordi  8634  oaabs  8664  omsmolem  8673  eceqoveq  8850  mapsnd  8921  dom2lem  9026  sbthlem9  9121  rexdif1en  9183  isinf  9263  frfi  9283  fiint  9325  fodomfib  9327  fofinf1o  9328  marypha1lem  9432  ordiso2  9516  unwdomg  9585  xpwdomg  9586  frr1  9770  ac5num  10122  cff1  10343  cfcoflem  10357  infpssrlem4  10391  isf32lem9  10446  isf34lem7  10464  fin1a2lem13  10497  fin1a2s  10499  hsmexlem4  10514  axdc2lem  10533  zorn2lem6  10586  axpowndlem2  10690  inttsk  10866  tskuni  10875  nqereu  11021  prcdnq  11085  addclprlem2  11109  ltexpri  11135  prlem936  11139  reclem2pr  11140  axsup  11392  add4  11538  ltleadd  11806  lt2mul2div  12202  nn2ge  12372  zextle  12779  fnn0ind  12805  xrlttr  13276  ifle  13334  xnn0lem1lt  13381  xaddass  13386  xmulasslem3  13423  xlemul1a  13425  xadddilem  13431  xrsupsslem  13444  xrinfmsslem  13445  supxrunb1  13456  supxrunb2  13457  ixxin  13500  difreicc  13622  iccsplit  13623  iccshftr  13624  iccshftl  13626  iccdil  13628  icccntr  13630  fzaddel  13699  fzadd2  13700  fzrev  13728  modadd1  14055  modmul1  14074  fsuppmapnn0fiub  14141  mulexp  14251  expadd  14254  expmul  14257  expnbnd  14383  bccl  14473  hashdom  14530  prsshashgt1  14562  hashfacen  14606  brfi1uzind  14660  wrdnval  14697  swrdccat3blem  14896  revccat  14923  2shfti  15242  sgn3da  15263  rexico  15530  cau3lem  15531  subcn2  15771  caucvgb  15856  iseraltlem1  15858  sumss  15899  fsumsplitsn  15919  incexclem  16014  supcvg  16034  mertenslem2  16063  fprodn0  16155  fprodsplitsn  16165  fprodle  16172  eftlcl  16284  reeftlcl  16285  rpnnen2lem6  16396  dvdsext  16500  3dvds  16510  sqoddm1div8z  16533  gcdcllem3  16680  dvdsexpim  16737  bezoutr1  16753  seq1st  16755  dvdslcm  16782  lcmeq0  16784  lcmcl  16785  lcmneg  16787  lcmdvds  16792  coprmgcdb  16833  dvdsprime  16871  pc2dvds  17066  prmpwdvds  17091  unbenlem  17095  infpnlem1  17097  1arith  17114  vdwmc2  17166  ramcl  17216  mrcuni  17804  isacs1i  17840  acsfn  17842  funcpropd  18086  curfcl  18415  curf2ndf  18430  mgmidpfod  18866  resmgmhm  18909  resmgmhm2b  18911  mgmhmco  18912  mgmhmima  18913  resmhm  19025  resmhm2b  19027  mhmco  19028  pwsdiagmhm  19036  gsumwsubmcl  19042  gsumwspan  19051  pwmnd  19152  dfgrp2  19182  subgint  19370  ghmmhmb  19450  resghm  19455  cntzmhm  19564  symgextf1lem  19643  f1omvdconj  19669  dfod2  19787  gexdvds  19807  subgpgp  19820  sylow1lem3  19823  frgpnabllem1  20096  dprdfeq0  20247  rhmimasubrnglem  20826  cntzsubrng  20828  cntzsubr  20867  isdrng2  21006  isdrng3lem1  21014  islmodd  21150  lsslss  21245  reslmhm2b  21338  rngqiprngimfo  21606  rhmpreimaprmidl  21644  psgnfix1  21913  psgndif  21917  copsgndif  21918  ocvocv  21986  frlmsslsp  22111  frlmlbs  22112  lindsenlbs  22166  psrbaglefi  22243  psrdi  22281  psrass23l  22283  psrass23  22285  evlsvvval  22411  rhmcomulmpl  22442  selvcllem5  22457  psdmul  22496  mptcoe1fsupp  22542  psropprmul  22564  ply1coe  22625  mamudi  22727  mamudir  22728  mat1dimelbas  22795  scmatmulcl  22842  scmatfo  22854  mulmarep1gsum2  22898  mdetunilem7  22942  mdetunilem9  22944  gsummatr01lem3  22981  smadiadetlem3  22992  matunitlindflem1  23003  matunitlindflem2  23004  cpmadugsumlemF  23203  leordtval  23540  cnpnei  23591  cnco  23593  cnss1  23603  cmpsub  23727  hauscmplem  23733  dissnlocfin  23857  ptbasid  23903  tx2cn  23938  upxp  23951  txindis  23962  xkoptsub  23982  xkopt  23983  trfbas2  24171  filconn  24211  trfil2  24215  filssufilg  24239  ufileu  24247  fixufil  24250  ufilen  24258  rnelfmlem  24280  flimclsi  24306  hauspwpwf1  24315  fclsopn  24342  fclsfnflim  24355  fclscmpi  24357  alexsubALTlem4  24378  ptcmplem5  24384  tgpmulg  24421  subgtgp  24433  tgpt0  24447  tsmsxplem2  24482  metss  24836  metustfbas  24885  dscopn  24901  xrsmopn  25141  cncfss  25229  icoopnst  25269  iccpnfcnv  25274  icccvx  25280  evth  25289  phtpycc  25321  pcohtpylem  25349  lmmbrf  25592  fgcfil  25601  caucfil  25613  cfilres  25626  bcth3  25661  cmscsscms  25703  ovolfioo  25797  ovolficc  25798  voliunlem3  25882  volcn  25936  mbflimsup  25996  mbfi1fseqlem5  26049  itg2seq  26072  bddiblnc  26171  dvnff  26252  dvnadd  26258  cpnord  26264  c1liplem1  26325  plypf1  26540  plyaddlem1  26541  plymullem1  26542  coeeulem  26552  coeidlem  26565  dgrle  26571  dgrnznn  26575  plycjlem  26604  elqaalem3  26653  ulmcaulem  26730  ulmcau  26731  psergf  26748  psercn2  26759  efopn  26995  abscxpbnd  27090  leibpi  27279  isppw2  27451  muinv  27529  bposlem3  27622  gausslemma2dlem4  27705  pntrmax  27900  pntpbnd1  27922  qabvexp  27962  madebday  28295  mulsrid  28508  bdayons  28671  peano5n0s  28714  bdaypw2n0bndlem  28858  bdayfinlem  28881  eqeelen  29491  colinearalglem4  29496  axcgrid  29503  axsegconlem1  29504  axsegconlem3  29506  ax5seglem1  29515  ax5seglem2  29516  ax5seglem9  29524  axcontlem2  29552  cusgrfilem2  30046  vtxdgfisf  30066  usgr2pthlem  30358  uspgrn2crct  30406  crctcshwlkn0  30419  wwlksnext  30491  wwlksnextproplem3  30509  eupth2lem3lem4  30841  frgr3vlem1  30883  frgr3vlem2  30884  3vfriswmgrlem  30887  frgrwopreglem5  30931  numclwwlk3lem2  30994  grpoidinvlem3  31117  grpoidinv  31119  grpoideu  31120  nmoub3i  31384  nmlno0lem  31404  nmlnoubi  31407  ipasslem3  31444  ipblnfi  31466  hvaddsub4  31689  his35  31699  shsel3  31926  chj4  32146  spansncol  32179  chscllem2  32249  5oalem2  32266  3oalem2  32274  hoaddcl  32369  adjsym  32444  cnvadj  32503  hhcno  32515  hhcnf  32516  nmopub2tALT  32520  unoplin  32531  counop  32532  nmfnleub2  32537  hmoplin  32553  brafnmul  32562  nmlnop0iALT  32606  nmopun  32625  nmophmi  32642  riesz3i  32673  riesz1  32676  cnlnadjlem2  32679  cnlnadjlem6  32683  adjmul  32703  adjadd  32704  bra11  32719  cnvbraval  32721  kbass5  32731  kbass6  32732  leop2  32735  leopadd  32743  leopmuli  32744  leoptri  32747  leopnmid  32749  nmopleid  32750  pj3si  32818  hstel2  32830  cvcon3  32895  dmdmd  32911  dmdbr5  32919  mdsl0  32921  mdslmd1lem1  32936  mdslmd1lem2  32937  mdslmd3i  32943  superpos  32965  chirredlem2  33002  chirredlem3  33003  mdsymlem3  33016  mdsymlem5  33018  mdsymlem6  33019  sumdmdlem  33029  cdjreui  33043  cdj1i  33044  cdj3i  33052  foresf1o  33151  2ndimaxp  33291  abfmpel  33300  fcomptf  33303  fcnvgreu  33317  fdifsuppconst  33333  xrge0infss  33402  xnn0gt0  33411  cycpm2tr  33730  elrgspnlem2  33854  elrgspnlem3  33855  intlidl  34020  mplvrpmga  34227  psrmonmul  34232  esplyfval0  34246  vieta  34262  lssdimle  34290  mdetpmtr1  34505  cmpcref  34532  xrge0iifcnv  34615  zrhcntr  34661  esumcst  34745  hasheuni  34767  esum2dlem  34774  esum2d  34775  sigaclcu2  34802  insiga  34820  unelldsys  34841  measres  34905  measdivcst  34907  volfiniune  34913  ddemeas  34919  actfunsnf1o  35283  fnrelpredd  35776  fineqvac  35844  fineqvnttrclselem1  35849  sconnpi1  36094  cvmsss2  36129  satfv1lem  36217  fmlaomn0  36245  gonarlem  36249  mrsubco  36376  dfon2lem6  36646  hfext  37030  elicc3  37201  fnessref  37241  bj-ismooredr2  38139  pibt2  38449  fin2solem  38638  fin2so  38639  poimirlem2  38649  poimirlem14  38661  poimirlem25  38672  poimirlem26  38673  poimirlem29  38676  poimirlem30  38677  broucube  38681  heicant  38682  mblfinlem2  38685  mblfinlem3  38686  mblfinlem4  38687  ex-ovoliunnfl  38690  mbfresfi  38693  cnambfre  38695  itg2addnclem  38698  itg2addnclem2  38699  itg2addnc  38701  ftc1anclem3  38722  ftc1anclem4  38723  ftc1anclem5  38724  ftc1anclem6  38725  ftc1anclem7  38726  ftc1anclem8  38727  ftc1anc  38728  indexdom  38777  filbcmb  38783  fdc  38788  incsequz  38791  metf1o  38798  caures  38803  bndss  38829  ismtycnv  38845  heiborlem1  38854  rrncmslem  38875  isdrngo2  39001  rngoisocnv  39024  unichnidl  39074  erimeq2  39804  ax12eq  40107  ax12el  40108  lshpset2N  40285  pmapglb2N  40937  pmapglb2xN  40938  pclfinN  41066  polval2N  41072  cdleme31fv2  41559  cdleme32fvcl  41606  cdleme48gfv  41703  tendoicl  41962  tendoipl  41963  diaglbN  42221  dochkr1  42644  dochkr1OLDN  42645  sumcubes  43479  expeq1d  43490  zaddcomlem  43636  zmulcomlem  43640  fiabv  43709  rhmcomulpsr  43719  evlselv  43726  fsuppind  43727  fsuppssind  43730  mhpind  43731  nacsfix  43832  eq0rabdioph  43896  diophren  43929  rencldnfilem  43936  pell1234qrdich  43977  jm2.24  44079  jm2.26lem3  44117  wepwsolem  44158  pwssplit4  44200  isnumbasgrplem3  44216  onexoegt  44355  onov0suclim  44385  cantnfresb  44435  omcl2  44444  ofoaid1  44469  ofoaid2  44470  grumnudlem  45378  cvgdvgrat  45406  ofsubid  45417  bcc0  45433  binomcxplemnn0  45442  uzwo4  46178  fiiuncl  46190  iunincfi  46217  nsstr  46218  rexanuz3  46219  iinssiin  46252  disjrnmpt2  46311  disjinfi  46315  choicefi  46322  difmap  46328  iunmapsn  46338  axccdom  46343  axccd  46349  rnmptlb  46363  rnmptbd2lem  46368  ssfiunibd  46433  supxrgelem  46457  suplesup  46459  xrlexaddrp  46472  xralrple2  46474  infxrunb2  46487  xralrple3  46493  xrralrecnnle  46502  xrralrecnnge  46509  supxrunb3  46518  unb2ltle  46533  rexabslelem  46536  supminfrnmpt  46563  infxrpnf  46564  supminfxr  46582  supminfxr2  46587  xrpnf  46603  pimxrneun  46606  cvgcaule  46609  iooiinicc  46662  ressioosup  46675  iooiinioc  46676  ressiooinf  46677  fsumsupp0  46698  divcnvg  46747  limcrecl  46749  sumnnodd  46750  islpcn  46757  lptre2pt  46758  limcresiooub  46760  limcresioolb  46761  limclner  46769  fnlimfvre  46792  allbutfifvre  46793  climinf3  46834  limsupmnflem  46838  limsupre3uzlem  46853  limsupreuzmpt  46857  climuzlem  46861  climisp  46864  climrescn  46866  climxrrelem  46867  climxrre  46868  climlimsupcex  46887  liminflelimsuplem  46893  limsupgtlem  46895  liminfvalxr  46901  liminfreuzlem  46920  liminfltlem  46922  liminflimsupclim  46925  xlimpnfxnegmnf  46932  liminflbuz2  46933  liminflimsupxrre  46935  cnrefiisplem  46947  xlimmnfvlem2  46951  xlimmnfv  46952  xlimpnfvlem2  46955  xlimpnfv  46956  xlimmnfmpt  46961  xlimpnfmpt  46962  climxlim2lem  46963  dfxlim2v  46965  xlimliminflimsup  46980  cncfuni  47004  icccncfext  47005  cncficcgt0  47006  cncfiooicclem1  47011  cncfiooiccre  47013  dvasinbx  47038  dvdsn1add  47057  dvnmul  47061  dvmptfprodlem  47062  dvnprodlem1  47064  dvnprodlem3  47066  iblspltprt  47091  itgioocnicc  47095  itgspltprt  47097  ismbl3  47104  stirlinglem5  47196  dirker2re  47210  dirkerper  47214  dirkertrigeq  47219  dirkercncflem2  47222  fourierdlem12  47237  fourierdlem15  47240  fourierdlem16  47241  fourierdlem20  47245  fourierdlem21  47246  fourierdlem22  47247  fourierdlem39  47264  fourierdlem40  47265  fourierdlem41  47266  fourierdlem42  47267  fourierdlem46  47270  fourierdlem49  47273  fourierdlem50  47274  fourierdlem57  47281  fourierdlem58  47282  fourierdlem59  47283  fourierdlem64  47288  fourierdlem65  47289  fourierdlem66  47290  fourierdlem68  47292  fourierdlem70  47294  fourierdlem71  47295  fourierdlem73  47297  fourierdlem78  47302  fourierdlem79  47303  fourierdlem80  47304  fourierdlem81  47305  fourierdlem82  47306  fourierdlem83  47307  fourierdlem87  47311  fourierdlem93  47317  fourierdlem95  47319  fourierdlem101  47325  fourierdlem103  47327  fourierdlem104  47328  fourierdlem111  47335  fourierdlem112  47336  sqwvfoura  47346  fourierswlem  47348  elaa2lem  47351  etransclem13  47365  etransclem23  47375  etransclem24  47376  etransclem32  47384  etransclem38  47390  etransclem46  47398  qndenserrnbllem  47412  rrxsnicc  47418  ioorrnopnlem  47422  prsal  47436  intsal  47448  salexct  47452  dfsalgen2  47459  issalnnd  47463  sge0rnre  47482  sge0val  47484  sge0z  47493  sge0revalmpt  47496  sge0tsms  47498  sge0pr  47512  sge0resplit  47524  sge0split  47527  sge0splitmpt  47529  sge0iunmptlemfi  47531  sge0iunmptlemre  47533  sge0fodjrnlem  47534  sge0iunmpt  47536  sge0rpcpnf  47539  sge0ltfirpmpt2  47544  sge0isum  47545  sge0xaddlem1  47551  sge0xaddlem2  47552  sge0pnffsumgt  47560  sge0gtfsumgt  47561  sge0seq  47564  sge0reuz  47565  nnfoctbdjlem  47573  nnfoctbdj  47574  meadjun  47580  meadjiunlem  47583  voliunsge0lem  47590  meaiuninc3v  47602  omeiunltfirp  47637  carageniuncllem2  47640  caratheodorylem1  47644  caratheodorylem2  47645  caratheodory  47646  isomenndlem  47648  isomennd  47649  hoicvr  47666  volicorescl  47671  ovnsubaddlem2  47689  hoidmvlelem2  47714  hoidmvlelem3  47715  hoidmvle  47718  ovnhoilem2  47720  hspdifhsp  47734  hoiqssbllem2  47741  hoiqssbllem3  47742  hspmbllem2  47745  ovnsubadd2lem  47763  ovolval4lem1  47767  vonvolmbl  47779  vonioo  47800  vonicc  47803  pimrecltpos  47826  issmfle  47863  smflimlem1  47889  smflimlem2  47890  smflimlem6  47894  smfresal  47906  smfrec  47907  smfmullem4  47912  smfpimcc  47926  smflimmpt  47928  smfsuplem1  47929  smfsuplem3  47931  smfsupmpt  47933  smfsupxr  47934  smfinflem  47935  smfinfmpt  47937  smflimsuplem4  47941  smflimsuplem5  47942  smflimsupmpt  47947  smfliminfmpt  47950  fsupdm  47960  finfdm  47964  smonoord  48555  lswn0  48634  poprelb  48714  fmtnoprmfac1  48758  fmtnofac2lem  48761  sbgoldbst  48984  isgrim  49088  gpgedgvtx0  49267  snlindsntorlem  49690  1arymaptf  49861  ipolubdm  50209  ipoglbdm  50212  setc1onsubc  50848  aacllem  51122