Theorem adantll 713

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 579	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  726  ad2ant2l  745  ad2ant2lr  747  ad5ant23  759  ad5ant24  760  ad5ant25  761  3adant1  1130  3ad2antl3  1187  ralcom2  3385  vtocl2d  3574  sbc2iegf  3886  sbcralt  3894  pofun  5626  poinxp  5780  xpdifid  6199  sossfld  6217  preddowncl  6364  tz7.7  6421  onfr  6434  ssimaex  7007  eqfnun  7070  fndmdif  7075  dffo4  7137  fompt  7152  fcompt  7167  fconst2g  7240  f1cofveqaeq  7295  2f1fvneq  7297  isores3  7371  fvmptopabOLD  7505  limsssuc  7887  el2mpocl  8127  1stconst  8141  2ndconst  8142  curry1  8145  curry2  8148  poseq  8199  soseq  8200  extmptsuppeq  8229  suppss  8235  suppss2  8241  onnseq  8400  oe0  8578  oesuclem  8581  oecl  8593  oaordi  8602  oawordri  8606  omordi  8622  omword2  8630  omlimcl  8634  odi  8635  omass  8636  oeoe  8655  nnaordi  8674  oaabs  8704  omsmolem  8713  eceqoveq  8880  mapsnd  8944  dom2lem  9052  sbthlem9  9157  rexdif1en  9224  php3OLD  9287  onomeneqOLD  9292  isinf  9323  isinfOLD  9324  frfi  9349  fiint  9394  fiintOLD  9395  fodomfib  9397  fodomfibOLD  9399  fofinf1o  9400  marypha1lem  9502  ordiso2  9584  unwdomg  9653  xpwdomg  9654  frr1  9828  ac5num  10105  cff1  10327  cfcoflem  10341  infpssrlem4  10375  isf32lem9  10430  isf34lem7  10448  fin1a2lem13  10481  fin1a2s  10483  hsmexlem4  10498  axdc2lem  10517  zorn2lem6  10570  axpowndlem2  10667  inttsk  10843  tskuni  10852  nqereu  10998  prcdnq  11062  addclprlem2  11086  ltexpri  11112  prlem936  11116  reclem2pr  11117  axsup  11365  add4  11510  ltleadd  11773  lt2mul2div  12173  nn2ge  12320  zextle  12716  fnn0ind  12742  xrlttr  13202  ifle  13259  xnn0lem1lt  13306  xaddass  13311  xmulasslem3  13348  xlemul1a  13350  xadddilem  13356  xrsupsslem  13369  xrinfmsslem  13370  supxrunb1  13381  supxrunb2  13382  ixxin  13424  difreicc  13544  iccsplit  13545  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  fzaddel  13618  fzadd2  13619  fzrev  13647  modadd1  13959  modmul1  13975  fsuppmapnn0fiub  14042  mulexp  14152  expadd  14155  expmul  14158  expnbnd  14281  bccl  14371  hashdom  14428  prsshashgt1  14459  hashfacen  14503  brfi1uzind  14557  wrdnval  14593  swrdccat3blem  14787  revccat  14814  2shfti  15129  rexico  15402  cau3lem  15403  subcn2  15641  caucvgb  15728  iseraltlem1  15730  sumss  15772  fsumsplitsn  15792  incexclem  15884  supcvg  15904  mertenslem2  15933  fprodn0  16027  fprodsplitsn  16037  fprodle  16044  eftlcl  16155  reeftlcl  16156  rpnnen2lem6  16267  dvdsext  16369  3dvds  16379  sqoddm1div8z  16402  gcdcllem3  16547  dvdsexpim  16602  bezoutr1  16616  seq1st  16618  dvdslcm  16645  lcmeq0  16647  lcmcl  16648  lcmneg  16650  lcmdvds  16655  coprmgcdb  16696  dvdsprime  16734  pc2dvds  16926  prmpwdvds  16951  unbenlem  16955  infpnlem1  16957  1arith  16974  vdwmc2  17026  ramcl  17076  mrcuni  17679  isacs1i  17715  acsfn  17717  funcpropd  17967  curfcl  18302  curf2ndf  18317  resmgmhm  18749  resmgmhm2b  18751  mgmhmco  18752  mgmhmima  18753  resmhm  18855  resmhm2b  18857  mhmco  18858  pwsdiagmhm  18866  gsumwsubmcl  18872  gsumwspan  18881  pwmnd  18972  dfgrp2  19002  subgint  19190  ghmmhmb  19267  resghm  19272  cntzmhm  19381  symgextf1lem  19462  f1omvdconj  19488  dfod2  19606  gexdvds  19626  subgpgp  19639  sylow1lem3  19642  frgpnabllem1  19915  dprdfeq0  20066  rhmimasubrnglem  20591  cntzsubrng  20593  cntzsubr  20634  isdrng2  20765  islmodd  20886  lsslss  20982  reslmhm2b  21076  rngqiprngimfo  21334  psgnfix1  21639  psgndif  21643  copsgndif  21644  ocvocv  21712  frlmsslsp  21839  frlmlbs  21840  psrbaglefi  21969  psrdi  22008  psrass23l  22010  psrass23  22012  psdmul  22193  mptcoe1fsupp  22238  psropprmul  22260  ply1coe  22323  rhmcomulmpl  22407  mamudi  22428  mamudir  22429  mat1dimelbas  22498  scmatmulcl  22545  scmatfo  22557  mulmarep1gsum2  22601  mdetunilem7  22645  mdetunilem9  22647  gsummatr01lem3  22684  smadiadetlem3  22695  cpmadugsumlemF  22903  leordtval  23242  cnpnei  23293  cnco  23295  cnss1  23305  cmpsub  23429  hauscmplem  23435  dissnlocfin  23558  ptbasid  23604  tx2cn  23639  upxp  23652  txindis  23663  xkoptsub  23683  xkopt  23684  trfbas2  23872  filconn  23912  trfil2  23916  filssufilg  23940  ufileu  23948  fixufil  23951  ufilen  23959  rnelfmlem  23981  flimclsi  24007  hauspwpwf1  24016  fclsopn  24043  fclsfnflim  24056  fclscmpi  24058  alexsubALTlem4  24079  ptcmplem5  24085  tgpmulg  24122  subgtgp  24134  tgpt0  24148  tsmsxplem2  24183  metss  24542  metustfbas  24591  dscopn  24607  xrsmopn  24853  cncfss  24944  icoopnst  24988  iccpnfcnv  24994  icccvx  25000  evth  25010  phtpycc  25042  pcohtpylem  25071  lmmbrf  25315  fgcfil  25324  caucfil  25336  cfilres  25349  bcth3  25384  cmscsscms  25426  ovolfioo  25521  ovolficc  25522  voliunlem3  25606  volcn  25660  mbflimsup  25720  mbfi1fseqlem5  25774  itg2seq  25797  bddiblnc  25897  dvnff  25979  dvnadd  25985  cpnord  25991  c1liplem1  26055  plypf1  26271  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeidlem  26296  dgrle  26302  dgrnznn  26306  plycjlem  26336  elqaalem3  26381  ulmcaulem  26455  ulmcau  26456  psergf  26473  psercn2  26484  psercn2OLD  26485  efopn  26718  abscxpbnd  26814  leibpi  27003  isppw2  27176  muinv  27254  bposlem3  27348  gausslemma2dlem4  27431  pntrmax  27626  pntpbnd1  27648  qabvexp  27688  madebday  27956  mulsrid  28157  peano5n0s  28342  zs12bday  28442  eqeelen  28937  colinearalglem4  28942  axcgrid  28949  axsegconlem1  28950  axsegconlem3  28952  ax5seglem1  28961  ax5seglem2  28962  ax5seglem9  28970  axcontlem2  28998  cusgrfilem2  29492  vtxdgfisf  29512  usgr2pthlem  29799  uspgrn2crct  29841  crctcshwlkn0  29854  wwlksnext  29926  wwlksnextproplem3  29944  eupth2lem3lem4  30263  frgr3vlem1  30305  frgr3vlem2  30306  3vfriswmgrlem  30309  frgrwopreglem5  30353  numclwwlk3lem2  30416  grpoidinvlem3  30538  grpoidinv  30540  grpoideu  30541  nmoub3i  30805  nmlno0lem  30825  nmlnoubi  30828  ipasslem3  30865  ipblnfi  30887  hvaddsub4  31110  his35  31120  shsel3  31347  chj4  31567  spansncol  31600  chscllem2  31670  5oalem2  31687  3oalem2  31695  hoaddcl  31790  adjsym  31865  cnvadj  31924  hhcno  31936  hhcnf  31937  nmopub2tALT  31941  unoplin  31952  counop  31953  nmfnleub2  31958  hmoplin  31974  brafnmul  31983  nmlnop0iALT  32027  nmopun  32046  nmophmi  32063  riesz3i  32094  riesz1  32097  cnlnadjlem2  32100  cnlnadjlem6  32104  adjmul  32124  adjadd  32125  bra11  32140  cnvbraval  32142  kbass5  32152  kbass6  32153  leop2  32156  leopadd  32164  leopmuli  32165  leoptri  32168  leopnmid  32170  nmopleid  32171  pj3si  32239  hstel2  32251  cvcon3  32316  dmdmd  32332  dmdbr5  32340  mdsl0  32342  mdslmd1lem1  32357  mdslmd1lem2  32358  mdslmd3i  32364  superpos  32386  chirredlem2  32423  chirredlem3  32424  mdsymlem3  32437  mdsymlem5  32439  mdsymlem6  32440  sumdmdlem  32450  cdjreui  32464  cdj1i  32465  cdj3i  32473  foresf1o  32532  2ndimaxp  32665  abfmpel  32673  fcomptf  32676  fcnvgreu  32691  fdifsuppconst  32701  xrge0infss  32767  xnn0gt0  32776  cycpm2tr  33112  intlidl  33413  rhmpreimaprmidl  33444  lssdimle  33620  mdetpmtr1  33769  cmpcref  33796  xrge0iifcnv  33879  esumcst  34027  hasheuni  34049  esum2dlem  34056  esum2d  34057  sigaclcu2  34084  insiga  34101  unelldsys  34122  measres  34186  measdivcst  34188  volfiniune  34194  ddemeas  34200  sgn3da  34506  actfunsnf1o  34581  fnrelpredd  35065  fineqvac  35073  sconnpi1  35207  cvmsss2  35242  satfv1lem  35330  fmlaomn0  35358  gonarlem  35362  mrsubco  35489  dfon2lem6  35752  hfext  36147  elicc3  36283  fnessref  36323  bj-ismooredr2  37076  pibt2  37383  fin2solem  37566  fin2so  37567  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem2  37582  poimirlem14  37594  poimirlem25  37605  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  broucube  37614  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ex-ovoliunnfl  37623  mbfresfi  37626  cnambfre  37628  itg2addnclem  37631  itg2addnclem2  37632  itg2addnc  37634  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  indexdom  37694  filbcmb  37700  fdc  37705  incsequz  37708  metf1o  37715  caures  37720  bndss  37746  ismtycnv  37762  heiborlem1  37771  rrncmslem  37792  isdrngo2  37918  rngoisocnv  37941  unichnidl  37991  erimeq2  38634  ax12eq  38897  ax12el  38898  lshpset2N  39075  pmapglb2N  39728  pmapglb2xN  39729  pclfinN  39857  polval2N  39863  cdleme31fv2  40350  cdleme32fvcl  40397  cdleme48gfv  40494  tendoicl  40753  tendoipl  40754  diaglbN  41012  dochkr1  41435  dochkr1OLDN  41436  sumcubes  42301  expeq1d  42311  zaddcomlem  42427  zmulcomlem  42431  fiabv  42491  rhmcomulpsr  42506  evlsvvval  42518  selvcllem5  42537  evlselv  42542  fsuppind  42545  fsuppssind  42548  mhpind  42549  nacsfix  42668  eq0rabdioph  42732  diophren  42769  rencldnfilem  42776  pell1234qrdich  42817  jm2.24  42920  jm2.26lem3  42958  wepwsolem  42999  pwssplit4  43046  isnumbasgrplem3  43062  onexoegt  43205  onov0suclim  43236  cantnfresb  43286  omcl2  43295  ofoaid1  43320  ofoaid2  43321  grumnudlem  44254  cvgdvgrat  44282  ofsubid  44293  bcc0  44309  binomcxplemnn0  44318  uzwo4  44955  fiiuncl  44967  iunincfi  44996  nsstr  44997  rexanuz3  44998  iinssiin  45031  disjrnmpt2  45095  disjinfi  45099  choicefi  45107  fsneq  45113  difmap  45114  iunmapsn  45124  axccdom  45129  axccd  45136  rnmptlb  45152  rnmptbd2lem  45157  ssfiunibd  45224  supxrgelem  45252  suplesup  45254  xrlexaddrp  45267  xralrple2  45269  infxrunb2  45283  xralrple3  45289  xrralrecnnle  45298  xrralrecnnge  45305  supxrunb3  45314  unb2ltle  45330  rexabslelem  45333  supminfrnmpt  45360  infxrpnf  45361  supminfxr  45379  supminfxr2  45384  xrpnf  45401  pimxrneun  45404  cvgcaule  45407  iooiinicc  45460  ressioosup  45473  iooiinioc  45474  ressiooinf  45475  fsumsupp0  45499  divcnvg  45548  limcrecl  45550  sumnnodd  45551  islpcn  45560  lptre2pt  45561  limcresiooub  45563  limcresioolb  45564  limclner  45572  fnlimfvre  45595  allbutfifvre  45596  climinf3  45637  limsupmnflem  45641  limsupre3uzlem  45656  limsupreuzmpt  45660  climuzlem  45664  climisp  45667  climrescn  45669  climxrrelem  45670  climxrre  45671  climlimsupcex  45690  liminflelimsuplem  45696  limsupgtlem  45698  liminfvalxr  45704  liminfreuzlem  45723  liminfltlem  45725  liminflimsupclim  45728  xlimpnfxnegmnf  45735  liminflbuz2  45736  liminflimsupxrre  45738  cnrefiisplem  45750  xlimmnfvlem2  45754  xlimmnfv  45755  xlimpnfvlem2  45758  xlimpnfv  45759  xlimmnfmpt  45764  xlimpnfmpt  45765  climxlim2lem  45766  dfxlim2v  45768  xlimliminflimsup  45783  cncfuni  45807  icccncfext  45808  cncficcgt0  45809  cncfiooicclem1  45814  cncfiooiccre  45816  dvasinbx  45841  dvdsn1add  45860  dvnmul  45864  dvmptfprodlem  45865  dvnprodlem1  45867  dvnprodlem3  45869  iblspltprt  45894  itgioocnicc  45898  itgspltprt  45900  ismbl3  45907  stirlinglem5  45999  dirker2re  46013  dirkerper  46017  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem12  46040  fourierdlem15  46043  fourierdlem16  46044  fourierdlem20  46048  fourierdlem21  46049  fourierdlem22  46050  fourierdlem39  46067  fourierdlem40  46068  fourierdlem41  46069  fourierdlem42  46070  fourierdlem46  46073  fourierdlem49  46076  fourierdlem50  46077  fourierdlem57  46084  fourierdlem58  46085  fourierdlem59  46086  fourierdlem64  46091  fourierdlem65  46092  fourierdlem66  46093  fourierdlem68  46095  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem78  46105  fourierdlem79  46106  fourierdlem80  46107  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem87  46114  fourierdlem93  46120  fourierdlem95  46122  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  sqwvfoura  46149  fourierswlem  46151  elaa2lem  46154  etransclem13  46168  etransclem23  46178  etransclem24  46179  etransclem32  46187  etransclem38  46193  etransclem46  46201  qndenserrnbllem  46215  rrxsnicc  46221  ioorrnopnlem  46225  prsal  46239  intsal  46251  salexct  46255  dfsalgen2  46262  issalnnd  46266  sge0rnre  46285  sge0val  46287  sge0z  46296  sge0revalmpt  46299  sge0tsms  46301  sge0pr  46315  sge0resplit  46327  sge0split  46330  sge0splitmpt  46332  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0fodjrnlem  46337  sge0iunmpt  46339  sge0rpcpnf  46342  sge0ltfirpmpt2  46347  sge0isum  46348  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0pnffsumgt  46363  sge0gtfsumgt  46364  sge0seq  46367  sge0reuz  46368  nnfoctbdjlem  46376  nnfoctbdj  46377  meadjun  46383  meadjiunlem  46386  voliunsge0lem  46393  meaiuninc3v  46405  omeiunltfirp  46440  carageniuncllem2  46443  caratheodorylem1  46447  caratheodorylem2  46448  caratheodory  46449  isomenndlem  46451  isomennd  46452  hoicvr  46469  volicorescl  46474  ovnsubaddlem2  46492  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvle  46521  ovnhoilem2  46523  hspdifhsp  46537  hoiqssbllem2  46544  hoiqssbllem3  46545  hspmbllem2  46548  ovnsubadd2lem  46566  ovolval4lem1  46570  vonvolmbl  46582  vonioo  46603  vonicc  46606  pimrecltpos  46629  issmfle  46666  smflimlem1  46692  smflimlem2  46693  smflimlem6  46697  smfresal  46709  smfrec  46710  smfmullem4  46715  smfpimcc  46729  smflimmpt  46731  smfsuplem1  46732  smfsuplem3  46734  smfsupmpt  46736  smfsupxr  46737  smfinflem  46738  smfinfmpt  46740  smflimsuplem4  46744  smflimsuplem5  46745  smflimsupmpt  46750  smfliminfmpt  46753  fsupdm  46763  finfdm  46767  smonoord  47245  lswn0  47318  poprelb  47398  fmtnoprmfac1  47439  fmtnofac2lem  47442  sbgoldbst  47652  isgrim  47752  snlindsntorlem  48199  1arymaptf  48375  ipolubdm  48659  ipoglbdm  48662  aacllem  48895