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  3349  vtocl2d  3521  sbc2iegf  3817  sbcralt  3824  pofun  5558  poinxp  5713  xpdifid  6134  sossfld  6152  preddowncl  6298  tz7.7  6351  onfr  6364  ssimaex  6927  eqfnun  6991  fndmdif  6996  dffo4  7057  fompt  7072  fcompt  7088  fconst2g  7159  f1cofveqaeq  7213  isores3  7291  limsssuc  7802  el2mpocl  8038  1stconst  8052  2ndconst  8053  curry1  8056  curry2  8059  poseq  8110  soseq  8111  extmptsuppeq  8140  suppss  8146  suppss2  8152  onnseq  8286  oe0  8459  oesuclem  8462  oecl  8474  oaordi  8483  oawordri  8487  omordi  8503  omword2  8511  omlimcl  8515  odi  8516  omass  8517  oeoe  8537  nnaordi  8556  oaabs  8586  omsmolem  8595  eceqoveq  8771  mapsnd  8836  dom2lem  8941  sbthlem9  9035  rexdif1en  9097  isinf  9177  frfi  9197  fiint  9239  fodomfib  9241  fodomfibOLD  9243  fofinf1o  9244  marypha1lem  9348  ordiso2  9432  unwdomg  9501  xpwdomg  9502  frr1  9683  ac5num  9958  cff1  10180  cfcoflem  10194  infpssrlem4  10228  isf32lem9  10283  isf34lem7  10301  fin1a2lem13  10334  fin1a2s  10336  hsmexlem4  10351  axdc2lem  10370  zorn2lem6  10423  axpowndlem2  10521  inttsk  10697  tskuni  10706  nqereu  10852  prcdnq  10916  addclprlem2  10940  ltexpri  10966  prlem936  10970  reclem2pr  10971  axsup  11220  add4  11366  ltleadd  11632  lt2mul2div  12032  nn2ge  12184  zextle  12577  fnn0ind  12603  xrlttr  13066  ifle  13124  xnn0lem1lt  13171  xaddass  13176  xmulasslem3  13213  xlemul1a  13215  xadddilem  13221  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  supxrunb2  13247  ixxin  13290  difreicc  13412  iccsplit  13413  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  fzaddel  13486  fzadd2  13487  fzrev  13515  modadd1  13840  modmul1  13859  fsuppmapnn0fiub  13926  mulexp  14036  expadd  14039  expmul  14042  expnbnd  14167  bccl  14257  hashdom  14314  prsshashgt1  14345  hashfacen  14389  brfi1uzind  14443  wrdnval  14480  swrdccat3blem  14674  revccat  14701  2shfti  15015  rexico  15289  cau3lem  15290  subcn2  15530  caucvgb  15615  iseraltlem1  15617  sumss  15659  fsumsplitsn  15679  incexclem  15771  supcvg  15791  mertenslem2  15820  fprodn0  15914  fprodsplitsn  15924  fprodle  15931  eftlcl  16044  reeftlcl  16045  rpnnen2lem6  16156  dvdsext  16260  3dvds  16270  sqoddm1div8z  16293  gcdcllem3  16440  dvdsexpim  16494  bezoutr1  16508  seq1st  16510  dvdslcm  16537  lcmeq0  16539  lcmcl  16540  lcmneg  16542  lcmdvds  16547  coprmgcdb  16588  dvdsprime  16626  pc2dvds  16819  prmpwdvds  16844  unbenlem  16848  infpnlem1  16850  1arith  16867  vdwmc2  16919  ramcl  16969  mrcuni  17556  isacs1i  17592  acsfn  17594  funcpropd  17838  curfcl  18167  curf2ndf  18182  resmgmhm  18648  resmgmhm2b  18650  mgmhmco  18651  mgmhmima  18652  resmhm  18757  resmhm2b  18759  mhmco  18760  pwsdiagmhm  18768  gsumwsubmcl  18774  gsumwspan  18783  pwmnd  18874  dfgrp2  18904  subgint  19092  ghmmhmb  19168  resghm  19173  cntzmhm  19282  symgextf1lem  19361  f1omvdconj  19387  dfod2  19505  gexdvds  19525  subgpgp  19538  sylow1lem3  19541  frgpnabllem1  19814  dprdfeq0  19965  rhmimasubrnglem  20510  cntzsubrng  20512  cntzsubr  20551  isdrng2  20688  islmodd  20829  lsslss  20924  reslmhm2b  21018  rngqiprngimfo  21268  psgnfix1  21565  psgndif  21569  copsgndif  21570  ocvocv  21638  frlmsslsp  21763  frlmlbs  21764  psrbaglefi  21894  psrdi  21932  psrass23l  21934  psrass23  21936  evlsvvval  22060  psdmul  22121  mptcoe1fsupp  22168  psropprmul  22190  ply1coe  22254  rhmcomulmpl  22338  mamudi  22359  mamudir  22360  mat1dimelbas  22427  scmatmulcl  22474  scmatfo  22486  mulmarep1gsum2  22530  mdetunilem7  22574  mdetunilem9  22576  gsummatr01lem3  22613  smadiadetlem3  22624  cpmadugsumlemF  22832  leordtval  23169  cnpnei  23220  cnco  23222  cnss1  23232  cmpsub  23356  hauscmplem  23362  dissnlocfin  23485  ptbasid  23531  tx2cn  23566  upxp  23579  txindis  23590  xkoptsub  23610  xkopt  23611  trfbas2  23799  filconn  23839  trfil2  23843  filssufilg  23867  ufileu  23875  fixufil  23878  ufilen  23886  rnelfmlem  23908  flimclsi  23934  hauspwpwf1  23943  fclsopn  23970  fclsfnflim  23983  fclscmpi  23985  alexsubALTlem4  24006  ptcmplem5  24012  tgpmulg  24049  subgtgp  24061  tgpt0  24075  tsmsxplem2  24110  metss  24464  metustfbas  24513  dscopn  24529  xrsmopn  24769  cncfss  24860  icoopnst  24904  iccpnfcnv  24910  icccvx  24916  evth  24926  phtpycc  24958  pcohtpylem  24987  lmmbrf  25230  fgcfil  25239  caucfil  25251  cfilres  25264  bcth3  25299  cmscsscms  25341  ovolfioo  25436  ovolficc  25437  voliunlem3  25521  volcn  25575  mbflimsup  25635  mbfi1fseqlem5  25688  itg2seq  25711  bddiblnc  25811  dvnff  25893  dvnadd  25899  cpnord  25905  c1liplem1  25969  plypf1  26185  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coeidlem  26210  dgrle  26216  dgrnznn  26220  plycjlem  26250  elqaalem3  26297  ulmcaulem  26371  ulmcau  26372  psergf  26389  psercn2  26400  psercn2OLD  26401  efopn  26635  abscxpbnd  26731  leibpi  26920  isppw2  27093  muinv  27171  bposlem3  27265  gausslemma2dlem4  27348  pntrmax  27543  pntpbnd1  27565  qabvexp  27605  madebday  27908  mulsrid  28121  bdayons  28284  peano5n0s  28327  bdaypw2n0bndlem  28471  bdayfinlem  28494  eqeelen  28989  colinearalglem4  28994  axcgrid  29001  axsegconlem1  29002  axsegconlem3  29004  ax5seglem1  29013  ax5seglem2  29014  ax5seglem9  29022  axcontlem2  29050  cusgrfilem2  29542  vtxdgfisf  29562  usgr2pthlem  29848  uspgrn2crct  29893  crctcshwlkn0  29906  wwlksnext  29978  wwlksnextproplem3  29996  eupth2lem3lem4  30318  frgr3vlem1  30360  frgr3vlem2  30361  3vfriswmgrlem  30364  frgrwopreglem5  30408  numclwwlk3lem2  30471  grpoidinvlem3  30594  grpoidinv  30596  grpoideu  30597  nmoub3i  30861  nmlno0lem  30881  nmlnoubi  30884  ipasslem3  30921  ipblnfi  30943  hvaddsub4  31166  his35  31176  shsel3  31403  chj4  31623  spansncol  31656  chscllem2  31726  5oalem2  31743  3oalem2  31751  hoaddcl  31846  adjsym  31921  cnvadj  31980  hhcno  31992  hhcnf  31993  nmopub2tALT  31997  unoplin  32008  counop  32009  nmfnleub2  32014  hmoplin  32030  brafnmul  32039  nmlnop0iALT  32083  nmopun  32102  nmophmi  32119  riesz3i  32150  riesz1  32153  cnlnadjlem2  32156  cnlnadjlem6  32160  adjmul  32180  adjadd  32181  bra11  32196  cnvbraval  32198  kbass5  32208  kbass6  32209  leop2  32212  leopadd  32220  leopmuli  32221  leoptri  32224  leopnmid  32226  nmopleid  32227  pj3si  32295  hstel2  32307  cvcon3  32372  dmdmd  32388  dmdbr5  32396  mdsl0  32398  mdslmd1lem1  32413  mdslmd1lem2  32414  mdslmd3i  32420  superpos  32442  chirredlem2  32479  chirredlem3  32480  mdsymlem3  32493  mdsymlem5  32495  mdsymlem6  32496  sumdmdlem  32506  cdjreui  32520  cdj1i  32521  cdj3i  32529  foresf1o  32591  2ndimaxp  32736  abfmpel  32745  fcomptf  32748  fcnvgreu  32762  fdifsuppconst  32779  xrge0infss  32851  xnn0gt0  32860  sgn3da  32926  cycpm2tr  33213  elrgspnlem2  33337  elrgspnlem3  33338  intlidl  33513  rhmpreimaprmidl  33544  mplvrpmga  33722  psrmonmul  33727  esplyfval0  33741  vieta  33757  lssdimle  33785  mdetpmtr1  34001  cmpcref  34028  xrge0iifcnv  34111  zrhcntr  34157  esumcst  34241  hasheuni  34263  esum2dlem  34270  esum2d  34271  sigaclcu2  34298  insiga  34315  unelldsys  34336  measres  34400  measdivcst  34402  volfiniune  34408  ddemeas  34414  actfunsnf1o  34782  fnrelpredd  35268  fineqvac  35294  fineqvnttrclselem1  35299  sconnpi1  35455  cvmsss2  35490  satfv1lem  35578  fmlaomn0  35606  gonarlem  35610  mrsubco  35737  dfon2lem6  36002  hfext  36399  elicc3  36533  fnessref  36573  bj-ismooredr2  37363  pibt2  37672  fin2solem  37857  fin2so  37858  lindsenlbs  37866  matunitlindflem1  37867  matunitlindflem2  37868  poimirlem2  37873  poimirlem14  37885  poimirlem25  37896  poimirlem26  37897  poimirlem29  37900  poimirlem30  37901  broucube  37905  heicant  37906  mblfinlem2  37909  mblfinlem3  37910  mblfinlem4  37911  ex-ovoliunnfl  37914  mbfresfi  37917  cnambfre  37919  itg2addnclem  37922  itg2addnclem2  37923  itg2addnc  37925  ftc1anclem3  37946  ftc1anclem4  37947  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anclem8  37951  ftc1anc  37952  indexdom  37985  filbcmb  37991  fdc  37996  incsequz  37999  metf1o  38006  caures  38011  bndss  38037  ismtycnv  38053  heiborlem1  38062  rrncmslem  38083  isdrngo2  38209  rngoisocnv  38232  unichnidl  38282  erimeq2  39014  ax12eq  39317  ax12el  39318  lshpset2N  39495  pmapglb2N  40147  pmapglb2xN  40148  pclfinN  40276  polval2N  40282  cdleme31fv2  40769  cdleme32fvcl  40816  cdleme48gfv  40913  tendoicl  41172  tendoipl  41173  diaglbN  41431  dochkr1  41854  dochkr1OLDN  41855  sumcubes  42683  expeq1d  42694  zaddcomlem  42833  zmulcomlem  42837  fiabv  42906  rhmcomulpsr  42919  selvcllem5  42940  evlselv  42945  fsuppind  42948  fsuppssind  42951  mhpind  42952  nacsfix  43069  eq0rabdioph  43133  diophren  43170  rencldnfilem  43177  pell1234qrdich  43218  jm2.24  43320  jm2.26lem3  43358  wepwsolem  43399  pwssplit4  43446  isnumbasgrplem3  43462  onexoegt  43601  onov0suclim  43631  cantnfresb  43681  omcl2  43690  ofoaid1  43715  ofoaid2  43716  grumnudlem  44641  cvgdvgrat  44669  ofsubid  44680  bcc0  44696  binomcxplemnn0  44705  uzwo4  45413  fiiuncl  45425  iunincfi  45453  nsstr  45454  rexanuz3  45455  iinssiin  45488  disjrnmpt2  45547  disjinfi  45551  choicefi  45558  fsneq  45564  difmap  45565  iunmapsn  45575  axccdom  45580  axccd  45587  rnmptlb  45601  rnmptbd2lem  45606  ssfiunibd  45671  supxrgelem  45696  suplesup  45698  xrlexaddrp  45711  xralrple2  45713  infxrunb2  45726  xralrple3  45732  xrralrecnnle  45741  xrralrecnnge  45748  supxrunb3  45757  unb2ltle  45773  rexabslelem  45776  supminfrnmpt  45803  infxrpnf  45804  supminfxr  45822  supminfxr2  45827  xrpnf  45843  pimxrneun  45846  cvgcaule  45849  iooiinicc  45902  ressioosup  45915  iooiinioc  45916  ressiooinf  45917  fsumsupp0  45938  divcnvg  45987  limcrecl  45989  sumnnodd  45990  islpcn  45997  lptre2pt  45998  limcresiooub  46000  limcresioolb  46001  limclner  46009  fnlimfvre  46032  allbutfifvre  46033  climinf3  46074  limsupmnflem  46078  limsupre3uzlem  46093  limsupreuzmpt  46097  climuzlem  46101  climisp  46104  climrescn  46106  climxrrelem  46107  climxrre  46108  climlimsupcex  46127  liminflelimsuplem  46133  limsupgtlem  46135  liminfvalxr  46141  liminfreuzlem  46160  liminfltlem  46162  liminflimsupclim  46165  xlimpnfxnegmnf  46172  liminflbuz2  46173  liminflimsupxrre  46175  cnrefiisplem  46187  xlimmnfvlem2  46191  xlimmnfv  46192  xlimpnfvlem2  46195  xlimpnfv  46196  xlimmnfmpt  46201  xlimpnfmpt  46202  climxlim2lem  46203  dfxlim2v  46205  xlimliminflimsup  46220  cncfuni  46244  icccncfext  46245  cncficcgt0  46246  cncfiooicclem1  46251  cncfiooiccre  46253  dvasinbx  46278  dvdsn1add  46297  dvnmul  46301  dvmptfprodlem  46302  dvnprodlem1  46304  dvnprodlem3  46306  iblspltprt  46331  itgioocnicc  46335  itgspltprt  46337  ismbl3  46344  stirlinglem5  46436  dirker2re  46450  dirkerper  46454  dirkertrigeq  46459  dirkercncflem2  46462  fourierdlem12  46477  fourierdlem15  46480  fourierdlem16  46481  fourierdlem20  46485  fourierdlem21  46486  fourierdlem22  46487  fourierdlem39  46504  fourierdlem40  46505  fourierdlem41  46506  fourierdlem42  46507  fourierdlem46  46510  fourierdlem49  46513  fourierdlem50  46514  fourierdlem57  46521  fourierdlem58  46522  fourierdlem59  46523  fourierdlem64  46528  fourierdlem65  46529  fourierdlem66  46530  fourierdlem68  46532  fourierdlem70  46534  fourierdlem71  46535  fourierdlem73  46537  fourierdlem78  46542  fourierdlem79  46543  fourierdlem80  46544  fourierdlem81  46545  fourierdlem82  46546  fourierdlem83  46547  fourierdlem87  46551  fourierdlem93  46557  fourierdlem95  46559  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem112  46576  sqwvfoura  46586  fourierswlem  46588  elaa2lem  46591  etransclem13  46605  etransclem23  46615  etransclem24  46616  etransclem32  46624  etransclem38  46630  etransclem46  46638  qndenserrnbllem  46652  rrxsnicc  46658  ioorrnopnlem  46662  prsal  46676  intsal  46688  salexct  46692  dfsalgen2  46699  issalnnd  46703  sge0rnre  46722  sge0val  46724  sge0z  46733  sge0revalmpt  46736  sge0tsms  46738  sge0pr  46752  sge0resplit  46764  sge0split  46767  sge0splitmpt  46769  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0fodjrnlem  46774  sge0iunmpt  46776  sge0rpcpnf  46779  sge0ltfirpmpt2  46784  sge0isum  46785  sge0xaddlem1  46791  sge0xaddlem2  46792  sge0pnffsumgt  46800  sge0gtfsumgt  46801  sge0seq  46804  sge0reuz  46805  nnfoctbdjlem  46813  nnfoctbdj  46814  meadjun  46820  meadjiunlem  46823  voliunsge0lem  46830  meaiuninc3v  46842  omeiunltfirp  46877  carageniuncllem2  46880  caratheodorylem1  46884  caratheodorylem2  46885  caratheodory  46886  isomenndlem  46888  isomennd  46889  hoicvr  46906  volicorescl  46911  ovnsubaddlem2  46929  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvle  46958  ovnhoilem2  46960  hspdifhsp  46974  hoiqssbllem2  46981  hoiqssbllem3  46982  hspmbllem2  46985  ovnsubadd2lem  47003  ovolval4lem1  47007  vonvolmbl  47019  vonioo  47040  vonicc  47043  pimrecltpos  47066  issmfle  47103  smflimlem1  47129  smflimlem2  47130  smflimlem6  47134  smfresal  47146  smfrec  47147  smfmullem4  47152  smfpimcc  47166  smflimmpt  47168  smfsuplem1  47169  smfsuplem3  47171  smfsupmpt  47173  smfsupxr  47174  smfinflem  47175  smfinfmpt  47177  smflimsuplem4  47181  smflimsuplem5  47182  smflimsupmpt  47187  smfliminfmpt  47190  fsupdm  47200  finfdm  47204  smonoord  47731  lswn0  47804  poprelb  47884  fmtnoprmfac1  47925  fmtnofac2lem  47928  sbgoldbst  48138  isgrim  48242  gpgedgvtx0  48421  snlindsntorlem  48830  1arymaptf  49001  ipolubdm  49346  ipoglbdm  49349  setc1onsubc  49961  aacllem  50160