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  3363  vtocl2d  3524  sbc2iegf  3813  sbcralt  3819  pofun  5577  poinxp  5732  xpdifid  6159  xpdifcnvepel  6160  sossfld  6178  preddowncl  6334  tz7.7  6387  onfr  6401  ssimaex  6968  fsneq  7032  eqfnun  7034  fndmdif  7039  dffo4  7101  fompt  7116  fcompt  7132  fconst2g  7207  f1cofveqaeq  7259  isores3  7341  limsssuc  7859  el2mpocl  8095  1stconst  8109  2ndconst  8110  curry1  8113  curry2  8116  poseq  8168  soseq  8169  extmptsuppeq  8198  suppss  8204  suppss2  8210  onnseq  8345  oe0  8523  oesuclem  8526  oecl  8538  oaordi  8547  oawordri  8551  omordi  8567  omword2  8575  omlimcl  8579  odi  8580  omass  8581  oeoe  8601  nnaordi  8620  oaabs  8650  omsmolem  8659  eceqoveq  8836  mapsnd  8907  dom2lem  9012  sbthlem9  9107  rexdif1en  9169  isinf  9249  frfi  9269  fiint  9311  fodomfib  9313  fofinf1o  9314  marypha1lem  9418  ordiso2  9502  unwdomg  9571  xpwdomg  9572  frr1  9756  ac5num  10108  cff1  10329  cfcoflem  10343  infpssrlem4  10377  isf32lem9  10432  isf34lem7  10450  fin1a2lem13  10483  fin1a2s  10485  hsmexlem4  10500  axdc2lem  10519  zorn2lem6  10572  axpowndlem2  10676  inttsk  10852  tskuni  10861  nqereu  11007  prcdnq  11071  addclprlem2  11095  ltexpri  11121  prlem936  11125  reclem2pr  11126  axsup  11378  add4  11524  ltleadd  11792  lt2mul2div  12188  nn2ge  12358  zextle  12765  fnn0ind  12791  xrlttr  13262  ifle  13320  xnn0lem1lt  13367  xaddass  13372  xmulasslem3  13409  xlemul1a  13411  xadddilem  13417  xrsupsslem  13430  xrinfmsslem  13431  supxrunb1  13442  supxrunb2  13443  ixxin  13486  difreicc  13608  iccsplit  13609  iccshftr  13610  iccshftl  13612  iccdil  13614  icccntr  13616  fzaddel  13685  fzadd2  13686  fzrev  13714  modadd1  14041  modmul1  14060  fsuppmapnn0fiub  14127  mulexp  14237  expadd  14240  expmul  14243  expnbnd  14369  bccl  14459  hashdom  14516  prsshashgt1  14548  hashfacen  14592  brfi1uzind  14646  wrdnval  14683  swrdccat3blem  14881  revccat  14908  2shfti  15226  sgn3da  15247  rexico  15514  cau3lem  15515  subcn2  15755  caucvgb  15840  iseraltlem1  15842  sumss  15883  fsumsplitsn  15903  incexclem  15998  supcvg  16018  mertenslem2  16047  fprodn0  16139  fprodsplitsn  16149  fprodle  16156  eftlcl  16268  reeftlcl  16269  rpnnen2lem6  16380  dvdsext  16484  3dvds  16494  sqoddm1div8z  16517  gcdcllem3  16664  dvdsexpim  16721  bezoutr1  16737  seq1st  16739  dvdslcm  16766  lcmeq0  16768  lcmcl  16769  lcmneg  16771  lcmdvds  16776  coprmgcdb  16817  dvdsprime  16855  pc2dvds  17050  prmpwdvds  17075  unbenlem  17079  infpnlem1  17081  1arith  17098  vdwmc2  17150  ramcl  17200  mrcuni  17788  isacs1i  17824  acsfn  17826  funcpropd  18070  curfcl  18399  curf2ndf  18414  mgmidpfod  18850  resmgmhm  18893  resmgmhm2b  18895  mgmhmco  18896  mgmhmima  18897  resmhm  19009  resmhm2b  19011  mhmco  19012  pwsdiagmhm  19020  gsumwsubmcl  19026  gsumwspan  19035  pwmnd  19136  dfgrp2  19166  subgint  19354  ghmmhmb  19434  resghm  19439  cntzmhm  19548  symgextf1lem  19627  f1omvdconj  19653  dfod2  19771  gexdvds  19791  subgpgp  19804  sylow1lem3  19807  frgpnabllem1  20080  dprdfeq0  20231  rhmimasubrnglem  20810  cntzsubrng  20812  cntzsubr  20851  isdrng2  20990  isdrng3lem1  20998  islmodd  21134  lsslss  21229  reslmhm2b  21322  rngqiprngimfo  21590  rhmpreimaprmidl  21628  psgnfix1  21897  psgndif  21901  copsgndif  21902  ocvocv  21970  frlmsslsp  22095  frlmlbs  22096  lindsenlbs  22150  psrbaglefi  22227  psrdi  22265  psrass23l  22267  psrass23  22269  evlsvvval  22395  rhmcomulmpl  22426  selvcllem5  22441  psdmul  22480  mptcoe1fsupp  22526  psropprmul  22548  ply1coe  22609  mamudi  22711  mamudir  22712  mat1dimelbas  22779  scmatmulcl  22826  scmatfo  22838  mulmarep1gsum2  22882  mdetunilem7  22926  mdetunilem9  22928  gsummatr01lem3  22965  smadiadetlem3  22976  matunitlindflem1  22987  matunitlindflem2  22988  cpmadugsumlemF  23187  leordtval  23524  cnpnei  23575  cnco  23577  cnss1  23587  cmpsub  23711  hauscmplem  23717  dissnlocfin  23841  ptbasid  23887  tx2cn  23922  upxp  23935  txindis  23946  xkoptsub  23966  xkopt  23967  trfbas2  24155  filconn  24195  trfil2  24199  filssufilg  24223  ufileu  24231  fixufil  24234  ufilen  24242  rnelfmlem  24264  flimclsi  24290  hauspwpwf1  24299  fclsopn  24326  fclsfnflim  24339  fclscmpi  24341  alexsubALTlem4  24362  ptcmplem5  24368  tgpmulg  24405  subgtgp  24417  tgpt0  24431  tsmsxplem2  24466  metss  24820  metustfbas  24869  dscopn  24885  xrsmopn  25125  cncfss  25213  icoopnst  25253  iccpnfcnv  25258  icccvx  25264  evth  25273  phtpycc  25305  pcohtpylem  25333  lmmbrf  25576  fgcfil  25585  caucfil  25597  cfilres  25610  bcth3  25645  cmscsscms  25687  ovolfioo  25781  ovolficc  25782  voliunlem3  25866  volcn  25920  mbflimsup  25980  mbfi1fseqlem5  26033  itg2seq  26056  bddiblnc  26155  dvnff  26236  dvnadd  26242  cpnord  26248  c1liplem1  26309  plypf1  26524  plyaddlem1  26525  plymullem1  26526  coeeulem  26536  coeidlem  26549  dgrle  26555  dgrnznn  26559  plycjlem  26588  elqaalem3  26637  ulmcaulem  26714  ulmcau  26715  psergf  26732  psercn2  26743  efopn  26979  abscxpbnd  27074  leibpi  27263  isppw2  27435  muinv  27513  bposlem3  27606  gausslemma2dlem4  27689  pntrmax  27884  pntpbnd1  27906  qabvexp  27946  madebday  28279  mulsrid  28492  bdayons  28655  peano5n0s  28698  bdaypw2n0bndlem  28842  bdayfinlem  28865  eqeelen  29475  colinearalglem4  29480  axcgrid  29487  axsegconlem1  29488  axsegconlem3  29490  ax5seglem1  29499  ax5seglem2  29500  ax5seglem9  29508  axcontlem2  29536  cusgrfilem2  30030  vtxdgfisf  30050  usgr2pthlem  30342  uspgrn2crct  30390  crctcshwlkn0  30403  wwlksnext  30475  wwlksnextproplem3  30493  eupth2lem3lem4  30825  frgr3vlem1  30867  frgr3vlem2  30868  3vfriswmgrlem  30871  frgrwopreglem5  30915  numclwwlk3lem2  30978  grpoidinvlem3  31101  grpoidinv  31103  grpoideu  31104  nmoub3i  31368  nmlno0lem  31388  nmlnoubi  31391  ipasslem3  31428  ipblnfi  31450  hvaddsub4  31673  his35  31683  shsel3  31910  chj4  32130  spansncol  32163  chscllem2  32233  5oalem2  32250  3oalem2  32258  hoaddcl  32353  adjsym  32428  cnvadj  32487  hhcno  32499  hhcnf  32500  nmopub2tALT  32504  unoplin  32515  counop  32516  nmfnleub2  32521  hmoplin  32537  brafnmul  32546  nmlnop0iALT  32590  nmopun  32609  nmophmi  32626  riesz3i  32657  riesz1  32660  cnlnadjlem2  32663  cnlnadjlem6  32667  adjmul  32687  adjadd  32688  bra11  32703  cnvbraval  32705  kbass5  32715  kbass6  32716  leop2  32719  leopadd  32727  leopmuli  32728  leoptri  32731  leopnmid  32733  nmopleid  32734  pj3si  32802  hstel2  32814  cvcon3  32879  dmdmd  32895  dmdbr5  32903  mdsl0  32905  mdslmd1lem1  32920  mdslmd1lem2  32921  mdslmd3i  32927  superpos  32949  chirredlem2  32986  chirredlem3  32987  mdsymlem3  33000  mdsymlem5  33002  mdsymlem6  33003  sumdmdlem  33013  cdjreui  33027  cdj1i  33028  cdj3i  33036  foresf1o  33093  2ndimaxp  33233  abfmpel  33242  fcomptf  33245  fcnvgreu  33259  fdifsuppconst  33275  xrge0infss  33345  xnn0gt0  33354  cycpm2tr  33673  elrgspnlem2  33797  elrgspnlem3  33798  intlidl  33963  mplvrpmga  34170  psrmonmul  34175  esplyfval0  34189  vieta  34205  lssdimle  34233  mdetpmtr1  34448  cmpcref  34475  xrge0iifcnv  34558  zrhcntr  34604  esumcst  34688  hasheuni  34710  esum2dlem  34717  esum2d  34718  sigaclcu2  34745  insiga  34763  unelldsys  34784  measres  34848  measdivcst  34850  volfiniune  34856  ddemeas  34862  actfunsnf1o  35226  fnrelpredd  35709  fineqvac  35767  fineqvnttrclselem1  35772  sconnpi1  35983  cvmsss2  36018  satfv1lem  36106  fmlaomn0  36134  gonarlem  36138  mrsubco  36265  dfon2lem6  36530  hfext  36914  elicc3  37085  fnessref  37125  bj-ismooredr2  38011  pibt2  38320  fin2solem  38509  fin2so  38510  poimirlem2  38520  poimirlem14  38532  poimirlem25  38543  poimirlem26  38544  poimirlem29  38547  poimirlem30  38548  broucube  38552  heicant  38553  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  ex-ovoliunnfl  38561  mbfresfi  38564  cnambfre  38566  itg2addnclem  38569  itg2addnclem2  38570  itg2addnc  38572  ftc1anclem3  38593  ftc1anclem4  38594  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  indexdom  38648  filbcmb  38654  fdc  38659  incsequz  38662  metf1o  38669  caures  38674  bndss  38700  ismtycnv  38716  heiborlem1  38725  rrncmslem  38746  isdrngo2  38872  rngoisocnv  38895  unichnidl  38945  erimeq2  39675  ax12eq  39978  ax12el  39979  lshpset2N  40156  pmapglb2N  40808  pmapglb2xN  40809  pclfinN  40937  polval2N  40943  cdleme31fv2  41430  cdleme32fvcl  41477  cdleme48gfv  41574  tendoicl  41833  tendoipl  41834  diaglbN  42092  dochkr1  42515  dochkr1OLDN  42516  sumcubes  43350  expeq1d  43361  zaddcomlem  43507  zmulcomlem  43511  fiabv  43580  rhmcomulpsr  43590  evlselv  43597  fsuppind  43598  fsuppssind  43601  mhpind  43602  nacsfix  43702  eq0rabdioph  43766  diophren  43799  rencldnfilem  43806  pell1234qrdich  43847  jm2.24  43949  jm2.26lem3  43987  wepwsolem  44028  pwssplit4  44075  isnumbasgrplem3  44091  onexoegt  44230  onov0suclim  44260  cantnfresb  44310  omcl2  44319  ofoaid1  44344  ofoaid2  44345  grumnudlem  45254  cvgdvgrat  45282  ofsubid  45293  bcc0  45309  binomcxplemnn0  45318  uzwo4  46039  fiiuncl  46051  iunincfi  46078  nsstr  46079  rexanuz3  46080  iinssiin  46113  disjrnmpt2  46172  disjinfi  46176  choicefi  46183  difmap  46189  iunmapsn  46199  axccdom  46204  axccd  46210  rnmptlb  46224  rnmptbd2lem  46229  ssfiunibd  46294  supxrgelem  46318  suplesup  46320  xrlexaddrp  46333  xralrple2  46335  infxrunb2  46348  xralrple3  46354  xrralrecnnle  46363  xrralrecnnge  46370  supxrunb3  46379  unb2ltle  46394  rexabslelem  46397  supminfrnmpt  46424  infxrpnf  46425  supminfxr  46443  supminfxr2  46448  xrpnf  46464  pimxrneun  46467  cvgcaule  46470  iooiinicc  46523  ressioosup  46536  iooiinioc  46537  ressiooinf  46538  fsumsupp0  46559  divcnvg  46608  limcrecl  46610  sumnnodd  46611  islpcn  46618  lptre2pt  46619  limcresiooub  46621  limcresioolb  46622  limclner  46630  fnlimfvre  46653  allbutfifvre  46654  climinf3  46695  limsupmnflem  46699  limsupre3uzlem  46714  limsupreuzmpt  46718  climuzlem  46722  climisp  46725  climrescn  46727  climxrrelem  46728  climxrre  46729  climlimsupcex  46748  liminflelimsuplem  46754  limsupgtlem  46756  liminfvalxr  46762  liminfreuzlem  46781  liminfltlem  46783  liminflimsupclim  46786  xlimpnfxnegmnf  46793  liminflbuz2  46794  liminflimsupxrre  46796  cnrefiisplem  46808  xlimmnfvlem2  46812  xlimmnfv  46813  xlimpnfvlem2  46816  xlimpnfv  46817  xlimmnfmpt  46822  xlimpnfmpt  46823  climxlim2lem  46824  dfxlim2v  46826  xlimliminflimsup  46841  cncfuni  46865  icccncfext  46866  cncficcgt0  46867  cncfiooicclem1  46872  cncfiooiccre  46874  dvasinbx  46899  dvdsn1add  46918  dvnmul  46922  dvmptfprodlem  46923  dvnprodlem1  46925  dvnprodlem3  46927  iblspltprt  46952  itgioocnicc  46956  itgspltprt  46958  ismbl3  46965  stirlinglem5  47057  dirker2re  47071  dirkerper  47075  dirkertrigeq  47080  dirkercncflem2  47083  fourierdlem12  47098  fourierdlem15  47101  fourierdlem16  47102  fourierdlem20  47106  fourierdlem21  47107  fourierdlem22  47108  fourierdlem39  47125  fourierdlem40  47126  fourierdlem41  47127  fourierdlem42  47128  fourierdlem46  47131  fourierdlem49  47134  fourierdlem50  47135  fourierdlem57  47142  fourierdlem58  47143  fourierdlem59  47144  fourierdlem64  47149  fourierdlem65  47150  fourierdlem66  47151  fourierdlem68  47153  fourierdlem70  47155  fourierdlem71  47156  fourierdlem73  47158  fourierdlem78  47163  fourierdlem79  47164  fourierdlem80  47165  fourierdlem81  47166  fourierdlem82  47167  fourierdlem83  47168  fourierdlem87  47172  fourierdlem93  47178  fourierdlem95  47180  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  sqwvfoura  47207  fourierswlem  47209  elaa2lem  47212  etransclem13  47226  etransclem23  47236  etransclem24  47237  etransclem32  47245  etransclem38  47251  etransclem46  47259  qndenserrnbllem  47273  rrxsnicc  47279  ioorrnopnlem  47283  prsal  47297  intsal  47309  salexct  47313  dfsalgen2  47320  issalnnd  47324  sge0rnre  47343  sge0val  47345  sge0z  47354  sge0revalmpt  47357  sge0tsms  47359  sge0pr  47373  sge0resplit  47385  sge0split  47388  sge0splitmpt  47390  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0fodjrnlem  47395  sge0iunmpt  47397  sge0rpcpnf  47400  sge0ltfirpmpt2  47405  sge0isum  47406  sge0xaddlem1  47412  sge0xaddlem2  47413  sge0pnffsumgt  47421  sge0gtfsumgt  47422  sge0seq  47425  sge0reuz  47426  nnfoctbdjlem  47434  nnfoctbdj  47435  meadjun  47441  meadjiunlem  47444  voliunsge0lem  47451  meaiuninc3v  47463  omeiunltfirp  47498  carageniuncllem2  47501  caratheodorylem1  47505  caratheodorylem2  47506  caratheodory  47507  isomenndlem  47509  isomennd  47510  hoicvr  47527  volicorescl  47532  ovnsubaddlem2  47550  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvle  47579  ovnhoilem2  47581  hspdifhsp  47595  hoiqssbllem2  47602  hoiqssbllem3  47603  hspmbllem2  47606  ovnsubadd2lem  47624  ovolval4lem1  47628  vonvolmbl  47640  vonioo  47661  vonicc  47664  pimrecltpos  47687  issmfle  47724  smflimlem1  47750  smflimlem2  47751  smflimlem6  47755  smfresal  47767  smfrec  47768  smfmullem4  47773  smfpimcc  47787  smflimmpt  47789  smfsuplem1  47790  smfsuplem3  47792  smfsupmpt  47794  smfsupxr  47795  smfinflem  47796  smfinfmpt  47798  smflimsuplem4  47802  smflimsuplem5  47803  smflimsupmpt  47808  smfliminfmpt  47811  fsupdm  47821  finfdm  47825  smonoord  48416  lswn0  48495  poprelb  48575  fmtnoprmfac1  48619  fmtnofac2lem  48622  sbgoldbst  48845  isgrim  48949  gpgedgvtx0  49128  snlindsntorlem  49551  1arymaptf  49722  ipolubdm  50064  ipoglbdm  50067  setc1onsubc  50679  aacllem  50908