Theorem adantll 714

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 580	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  727  ad2ant2l  746  ad2ant2lr  748  ad5ant23  759  ad5ant24  760  ad5ant25  761  3adant1  1130  3ad2antl3  1188  ralcom2  3343  vtocl2d  3515  sbc2iegf  3811  sbcralt  3818  pofun  5537  poinxp  5692  xpdifid  6110  sossfld  6128  preddowncl  6274  tz7.7  6327  onfr  6340  ssimaex  6902  eqfnun  6965  fndmdif  6970  dffo4  7031  fompt  7046  fcompt  7061  fconst2g  7132  f1cofveqaeq  7186  isores3  7264  limsssuc  7775  el2mpocl  8011  1stconst  8025  2ndconst  8026  curry1  8029  curry2  8032  poseq  8083  soseq  8084  extmptsuppeq  8113  suppss  8119  suppss2  8125  onnseq  8259  oe0  8432  oesuclem  8435  oecl  8447  oaordi  8456  oawordri  8460  omordi  8476  omword2  8484  omlimcl  8488  odi  8489  omass  8490  oeoe  8509  nnaordi  8528  oaabs  8558  omsmolem  8567  eceqoveq  8741  mapsnd  8805  dom2lem  8909  sbthlem9  9003  rexdif1en  9065  isinf  9144  frfi  9164  fiint  9206  fodomfib  9208  fodomfibOLD  9210  fofinf1o  9211  marypha1lem  9312  ordiso2  9396  unwdomg  9465  xpwdomg  9466  frr1  9647  ac5num  9922  cff1  10144  cfcoflem  10158  infpssrlem4  10192  isf32lem9  10247  isf34lem7  10265  fin1a2lem13  10298  fin1a2s  10300  hsmexlem4  10315  axdc2lem  10334  zorn2lem6  10387  axpowndlem2  10484  inttsk  10660  tskuni  10669  nqereu  10815  prcdnq  10879  addclprlem2  10903  ltexpri  10929  prlem936  10933  reclem2pr  10934  axsup  11183  add4  11329  ltleadd  11595  lt2mul2div  11995  nn2ge  12147  zextle  12541  fnn0ind  12567  xrlttr  13034  ifle  13091  xnn0lem1lt  13138  xaddass  13143  xmulasslem3  13180  xlemul1a  13182  xadddilem  13188  xrsupsslem  13201  xrinfmsslem  13202  supxrunb1  13213  supxrunb2  13214  ixxin  13257  difreicc  13379  iccsplit  13380  iccshftr  13381  iccshftl  13383  iccdil  13385  icccntr  13387  fzaddel  13453  fzadd2  13454  fzrev  13482  modadd1  13807  modmul1  13826  fsuppmapnn0fiub  13893  mulexp  14003  expadd  14006  expmul  14009  expnbnd  14134  bccl  14224  hashdom  14281  prsshashgt1  14312  hashfacen  14356  brfi1uzind  14410  wrdnval  14447  swrdccat3blem  14641  revccat  14668  2shfti  14982  rexico  15256  cau3lem  15257  subcn2  15497  caucvgb  15582  iseraltlem1  15584  sumss  15626  fsumsplitsn  15646  incexclem  15738  supcvg  15758  mertenslem2  15787  fprodn0  15881  fprodsplitsn  15891  fprodle  15898  eftlcl  16011  reeftlcl  16012  rpnnen2lem6  16123  dvdsext  16227  3dvds  16237  sqoddm1div8z  16260  gcdcllem3  16407  dvdsexpim  16461  bezoutr1  16475  seq1st  16477  dvdslcm  16504  lcmeq0  16506  lcmcl  16507  lcmneg  16509  lcmdvds  16514  coprmgcdb  16555  dvdsprime  16593  pc2dvds  16786  prmpwdvds  16811  unbenlem  16815  infpnlem1  16817  1arith  16834  vdwmc2  16886  ramcl  16936  mrcuni  17522  isacs1i  17558  acsfn  17560  funcpropd  17804  curfcl  18133  curf2ndf  18148  resmgmhm  18614  resmgmhm2b  18616  mgmhmco  18617  mgmhmima  18618  resmhm  18723  resmhm2b  18725  mhmco  18726  pwsdiagmhm  18734  gsumwsubmcl  18740  gsumwspan  18749  pwmnd  18840  dfgrp2  18870  subgint  19058  ghmmhmb  19134  resghm  19139  cntzmhm  19248  symgextf1lem  19327  f1omvdconj  19353  dfod2  19471  gexdvds  19491  subgpgp  19504  sylow1lem3  19507  frgpnabllem1  19780  dprdfeq0  19931  rhmimasubrnglem  20475  cntzsubrng  20477  cntzsubr  20516  isdrng2  20653  islmodd  20794  lsslss  20889  reslmhm2b  20983  rngqiprngimfo  21233  psgnfix1  21530  psgndif  21534  copsgndif  21535  ocvocv  21603  frlmsslsp  21728  frlmlbs  21729  psrbaglefi  21858  psrdi  21897  psrass23l  21899  psrass23  21901  psdmul  22076  mptcoe1fsupp  22123  psropprmul  22145  ply1coe  22208  rhmcomulmpl  22292  mamudi  22313  mamudir  22314  mat1dimelbas  22381  scmatmulcl  22428  scmatfo  22440  mulmarep1gsum2  22484  mdetunilem7  22528  mdetunilem9  22530  gsummatr01lem3  22567  smadiadetlem3  22578  cpmadugsumlemF  22786  leordtval  23123  cnpnei  23174  cnco  23176  cnss1  23186  cmpsub  23310  hauscmplem  23316  dissnlocfin  23439  ptbasid  23485  tx2cn  23520  upxp  23533  txindis  23544  xkoptsub  23564  xkopt  23565  trfbas2  23753  filconn  23793  trfil2  23797  filssufilg  23821  ufileu  23829  fixufil  23832  ufilen  23840  rnelfmlem  23862  flimclsi  23888  hauspwpwf1  23897  fclsopn  23924  fclsfnflim  23937  fclscmpi  23939  alexsubALTlem4  23960  ptcmplem5  23966  tgpmulg  24003  subgtgp  24015  tgpt0  24029  tsmsxplem2  24064  metss  24418  metustfbas  24467  dscopn  24483  xrsmopn  24723  cncfss  24814  icoopnst  24858  iccpnfcnv  24864  icccvx  24870  evth  24880  phtpycc  24912  pcohtpylem  24941  lmmbrf  25184  fgcfil  25193  caucfil  25205  cfilres  25218  bcth3  25253  cmscsscms  25295  ovolfioo  25390  ovolficc  25391  voliunlem3  25475  volcn  25529  mbflimsup  25589  mbfi1fseqlem5  25642  itg2seq  25665  bddiblnc  25765  dvnff  25847  dvnadd  25853  cpnord  25859  c1liplem1  25923  plypf1  26139  plyaddlem1  26140  plymullem1  26141  coeeulem  26151  coeidlem  26164  dgrle  26170  dgrnznn  26174  plycjlem  26204  elqaalem3  26251  ulmcaulem  26325  ulmcau  26326  psergf  26343  psercn2  26354  psercn2OLD  26355  efopn  26589  abscxpbnd  26685  leibpi  26874  isppw2  27047  muinv  27125  bposlem3  27219  gausslemma2dlem4  27302  pntrmax  27497  pntpbnd1  27519  qabvexp  27559  madebday  27840  mulsrid  28047  bdayon  28204  peano5n0s  28243  zs12bday  28389  eqeelen  28877  colinearalglem4  28882  axcgrid  28889  axsegconlem1  28890  axsegconlem3  28892  ax5seglem1  28901  ax5seglem2  28902  ax5seglem9  28910  axcontlem2  28938  cusgrfilem2  29430  vtxdgfisf  29450  usgr2pthlem  29736  uspgrn2crct  29781  crctcshwlkn0  29794  wwlksnext  29866  wwlksnextproplem3  29884  eupth2lem3lem4  30203  frgr3vlem1  30245  frgr3vlem2  30246  3vfriswmgrlem  30249  frgrwopreglem5  30293  numclwwlk3lem2  30356  grpoidinvlem3  30478  grpoidinv  30480  grpoideu  30481  nmoub3i  30745  nmlno0lem  30765  nmlnoubi  30768  ipasslem3  30805  ipblnfi  30827  hvaddsub4  31050  his35  31060  shsel3  31287  chj4  31507  spansncol  31540  chscllem2  31610  5oalem2  31627  3oalem2  31635  hoaddcl  31730  adjsym  31805  cnvadj  31864  hhcno  31876  hhcnf  31877  nmopub2tALT  31881  unoplin  31892  counop  31893  nmfnleub2  31898  hmoplin  31914  brafnmul  31923  nmlnop0iALT  31967  nmopun  31986  nmophmi  32003  riesz3i  32034  riesz1  32037  cnlnadjlem2  32040  cnlnadjlem6  32044  adjmul  32064  adjadd  32065  bra11  32080  cnvbraval  32082  kbass5  32092  kbass6  32093  leop2  32096  leopadd  32104  leopmuli  32105  leoptri  32108  leopnmid  32110  nmopleid  32111  pj3si  32179  hstel2  32191  cvcon3  32256  dmdmd  32272  dmdbr5  32280  mdsl0  32282  mdslmd1lem1  32297  mdslmd1lem2  32298  mdslmd3i  32304  superpos  32326  chirredlem2  32363  chirredlem3  32364  mdsymlem3  32377  mdsymlem5  32379  mdsymlem6  32380  sumdmdlem  32390  cdjreui  32404  cdj1i  32405  cdj3i  32413  foresf1o  32476  2ndimaxp  32620  abfmpel  32629  fcomptf  32632  fcnvgreu  32647  fdifsuppconst  32662  xrge0infss  32735  xnn0gt0  32744  sgn3da  32809  cycpm2tr  33080  elrgspnlem2  33202  elrgspnlem3  33203  intlidl  33377  rhmpreimaprmidl  33408  mplvrpmga  33567  lssdimle  33612  mdetpmtr1  33828  cmpcref  33855  xrge0iifcnv  33938  zrhcntr  33984  esumcst  34068  hasheuni  34090  esum2dlem  34097  esum2d  34098  sigaclcu2  34125  insiga  34142  unelldsys  34163  measres  34227  measdivcst  34229  volfiniune  34235  ddemeas  34241  actfunsnf1o  34609  fnrelpredd  35094  fineqvac  35131  fineqvnttrclselem1  35133  sconnpi1  35275  cvmsss2  35310  satfv1lem  35398  fmlaomn0  35426  gonarlem  35430  mrsubco  35557  dfon2lem6  35822  hfext  36217  elicc3  36351  fnessref  36391  bj-ismooredr2  37144  pibt2  37451  fin2solem  37646  fin2so  37647  lindsenlbs  37655  matunitlindflem1  37656  matunitlindflem2  37657  poimirlem2  37662  poimirlem14  37674  poimirlem25  37685  poimirlem26  37686  poimirlem29  37689  poimirlem30  37690  broucube  37694  heicant  37695  mblfinlem2  37698  mblfinlem3  37699  mblfinlem4  37700  ex-ovoliunnfl  37703  mbfresfi  37706  cnambfre  37708  itg2addnclem  37711  itg2addnclem2  37712  itg2addnc  37714  ftc1anclem3  37735  ftc1anclem4  37736  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  indexdom  37774  filbcmb  37780  fdc  37785  incsequz  37788  metf1o  37795  caures  37800  bndss  37826  ismtycnv  37842  heiborlem1  37851  rrncmslem  37872  isdrngo2  37998  rngoisocnv  38021  unichnidl  38071  erimeq2  38716  ax12eq  38980  ax12el  38981  lshpset2N  39158  pmapglb2N  39810  pmapglb2xN  39811  pclfinN  39939  polval2N  39945  cdleme31fv2  40432  cdleme32fvcl  40479  cdleme48gfv  40576  tendoicl  40835  tendoipl  40836  diaglbN  41094  dochkr1  41517  dochkr1OLDN  41518  sumcubes  42346  expeq1d  42357  zaddcomlem  42496  zmulcomlem  42500  fiabv  42569  rhmcomulpsr  42584  evlsvvval  42596  selvcllem5  42615  evlselv  42620  fsuppind  42623  fsuppssind  42626  mhpind  42627  nacsfix  42745  eq0rabdioph  42809  diophren  42846  rencldnfilem  42853  pell1234qrdich  42894  jm2.24  42996  jm2.26lem3  43034  wepwsolem  43075  pwssplit4  43122  isnumbasgrplem3  43138  onexoegt  43277  onov0suclim  43307  cantnfresb  43357  omcl2  43366  ofoaid1  43391  ofoaid2  43392  grumnudlem  44318  cvgdvgrat  44346  ofsubid  44357  bcc0  44373  binomcxplemnn0  44382  uzwo4  45090  fiiuncl  45102  iunincfi  45131  nsstr  45132  rexanuz3  45133  iinssiin  45166  disjrnmpt2  45225  disjinfi  45229  choicefi  45237  fsneq  45243  difmap  45244  iunmapsn  45254  axccdom  45259  axccd  45266  rnmptlb  45280  rnmptbd2lem  45285  ssfiunibd  45350  supxrgelem  45376  suplesup  45378  xrlexaddrp  45391  xralrple2  45393  infxrunb2  45406  xralrple3  45412  xrralrecnnle  45421  xrralrecnnge  45428  supxrunb3  45437  unb2ltle  45453  rexabslelem  45456  supminfrnmpt  45483  infxrpnf  45484  supminfxr  45502  supminfxr2  45507  xrpnf  45523  pimxrneun  45526  cvgcaule  45529  iooiinicc  45582  ressioosup  45595  iooiinioc  45596  ressiooinf  45597  fsumsupp0  45618  divcnvg  45667  limcrecl  45669  sumnnodd  45670  islpcn  45677  lptre2pt  45678  limcresiooub  45680  limcresioolb  45681  limclner  45689  fnlimfvre  45712  allbutfifvre  45713  climinf3  45754  limsupmnflem  45758  limsupre3uzlem  45773  limsupreuzmpt  45777  climuzlem  45781  climisp  45784  climrescn  45786  climxrrelem  45787  climxrre  45788  climlimsupcex  45807  liminflelimsuplem  45813  limsupgtlem  45815  liminfvalxr  45821  liminfreuzlem  45840  liminfltlem  45842  liminflimsupclim  45845  xlimpnfxnegmnf  45852  liminflbuz2  45853  liminflimsupxrre  45855  cnrefiisplem  45867  xlimmnfvlem2  45871  xlimmnfv  45872  xlimpnfvlem2  45875  xlimpnfv  45876  xlimmnfmpt  45881  xlimpnfmpt  45882  climxlim2lem  45883  dfxlim2v  45885  xlimliminflimsup  45900  cncfuni  45924  icccncfext  45925  cncficcgt0  45926  cncfiooicclem1  45931  cncfiooiccre  45933  dvasinbx  45958  dvdsn1add  45977  dvnmul  45981  dvmptfprodlem  45982  dvnprodlem1  45984  dvnprodlem3  45986  iblspltprt  46011  itgioocnicc  46015  itgspltprt  46017  ismbl3  46024  stirlinglem5  46116  dirker2re  46130  dirkerper  46134  dirkertrigeq  46139  dirkercncflem2  46142  fourierdlem12  46157  fourierdlem15  46160  fourierdlem16  46161  fourierdlem20  46165  fourierdlem21  46166  fourierdlem22  46167  fourierdlem39  46184  fourierdlem40  46185  fourierdlem41  46186  fourierdlem42  46187  fourierdlem46  46190  fourierdlem49  46193  fourierdlem50  46194  fourierdlem57  46201  fourierdlem58  46202  fourierdlem59  46203  fourierdlem64  46208  fourierdlem65  46209  fourierdlem66  46210  fourierdlem68  46212  fourierdlem70  46214  fourierdlem71  46215  fourierdlem73  46217  fourierdlem78  46222  fourierdlem79  46223  fourierdlem80  46224  fourierdlem81  46225  fourierdlem82  46226  fourierdlem83  46227  fourierdlem87  46231  fourierdlem93  46237  fourierdlem95  46239  fourierdlem101  46245  fourierdlem103  46247  fourierdlem104  46248  fourierdlem111  46255  fourierdlem112  46256  sqwvfoura  46266  fourierswlem  46268  elaa2lem  46271  etransclem13  46285  etransclem23  46295  etransclem24  46296  etransclem32  46304  etransclem38  46310  etransclem46  46318  qndenserrnbllem  46332  rrxsnicc  46338  ioorrnopnlem  46342  prsal  46356  intsal  46368  salexct  46372  dfsalgen2  46379  issalnnd  46383  sge0rnre  46402  sge0val  46404  sge0z  46413  sge0revalmpt  46416  sge0tsms  46418  sge0pr  46432  sge0resplit  46444  sge0split  46447  sge0splitmpt  46449  sge0iunmptlemfi  46451  sge0iunmptlemre  46453  sge0fodjrnlem  46454  sge0iunmpt  46456  sge0rpcpnf  46459  sge0ltfirpmpt2  46464  sge0isum  46465  sge0xaddlem1  46471  sge0xaddlem2  46472  sge0pnffsumgt  46480  sge0gtfsumgt  46481  sge0seq  46484  sge0reuz  46485  nnfoctbdjlem  46493  nnfoctbdj  46494  meadjun  46500  meadjiunlem  46503  voliunsge0lem  46510  meaiuninc3v  46522  omeiunltfirp  46557  carageniuncllem2  46560  caratheodorylem1  46564  caratheodorylem2  46565  caratheodory  46566  isomenndlem  46568  isomennd  46569  hoicvr  46586  volicorescl  46591  ovnsubaddlem2  46609  hoidmvlelem2  46634  hoidmvlelem3  46635  hoidmvle  46638  ovnhoilem2  46640  hspdifhsp  46654  hoiqssbllem2  46661  hoiqssbllem3  46662  hspmbllem2  46665  ovnsubadd2lem  46683  ovolval4lem1  46687  vonvolmbl  46699  vonioo  46720  vonicc  46723  pimrecltpos  46746  issmfle  46783  smflimlem1  46809  smflimlem2  46810  smflimlem6  46814  smfresal  46826  smfrec  46827  smfmullem4  46832  smfpimcc  46846  smflimmpt  46848  smfsuplem1  46849  smfsuplem3  46851  smfsupmpt  46853  smfsupxr  46854  smfinflem  46855  smfinfmpt  46857  smflimsuplem4  46861  smflimsuplem5  46862  smflimsupmpt  46867  smfliminfmpt  46870  fsupdm  46880  finfdm  46884  smonoord  47402  lswn0  47475  poprelb  47555  fmtnoprmfac1  47596  fmtnofac2lem  47599  sbgoldbst  47809  isgrim  47913  gpgedgvtx0  48092  snlindsntorlem  48502  1arymaptf  48673  ipolubdm  49018  ipoglbdm  49021  setc1onsubc  49634  aacllem  49833