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  3353  vtocl2d  3531  sbc2iegf  3831  sbcralt  3838  pofun  5567  poinxp  5722  xpdifid  6144  sossfld  6162  preddowncl  6308  tz7.7  6361  onfr  6374  ssimaex  6949  eqfnun  7012  fndmdif  7017  dffo4  7078  fompt  7093  fcompt  7108  fconst2g  7180  f1cofveqaeq  7235  isores3  7313  fvmptopabOLD  7447  limsssuc  7829  el2mpocl  8068  1stconst  8082  2ndconst  8083  curry1  8086  curry2  8089  poseq  8140  soseq  8141  extmptsuppeq  8170  suppss  8176  suppss2  8182  onnseq  8316  oe0  8489  oesuclem  8492  oecl  8504  oaordi  8513  oawordri  8517  omordi  8533  omword2  8541  omlimcl  8545  odi  8546  omass  8547  oeoe  8566  nnaordi  8585  oaabs  8615  omsmolem  8624  eceqoveq  8798  mapsnd  8862  dom2lem  8966  sbthlem9  9065  rexdif1en  9128  isinf  9214  isinfOLD  9215  frfi  9239  fiint  9284  fiintOLD  9285  fodomfib  9287  fodomfibOLD  9289  fofinf1o  9290  marypha1lem  9391  ordiso2  9475  unwdomg  9544  xpwdomg  9545  frr1  9719  ac5num  9996  cff1  10218  cfcoflem  10232  infpssrlem4  10266  isf32lem9  10321  isf34lem7  10339  fin1a2lem13  10372  fin1a2s  10374  hsmexlem4  10389  axdc2lem  10408  zorn2lem6  10461  axpowndlem2  10558  inttsk  10734  tskuni  10743  nqereu  10889  prcdnq  10953  addclprlem2  10977  ltexpri  11003  prlem936  11007  reclem2pr  11008  axsup  11256  add4  11402  ltleadd  11668  lt2mul2div  12068  nn2ge  12220  zextle  12614  fnn0ind  12640  xrlttr  13107  ifle  13164  xnn0lem1lt  13211  xaddass  13216  xmulasslem3  13253  xlemul1a  13255  xadddilem  13261  xrsupsslem  13274  xrinfmsslem  13275  supxrunb1  13286  supxrunb2  13287  ixxin  13330  difreicc  13452  iccsplit  13453  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  fzaddel  13526  fzadd2  13527  fzrev  13555  modadd1  13877  modmul1  13896  fsuppmapnn0fiub  13963  mulexp  14073  expadd  14076  expmul  14079  expnbnd  14204  bccl  14294  hashdom  14351  prsshashgt1  14382  hashfacen  14426  brfi1uzind  14480  wrdnval  14517  swrdccat3blem  14711  revccat  14738  2shfti  15053  rexico  15327  cau3lem  15328  subcn2  15568  caucvgb  15653  iseraltlem1  15655  sumss  15697  fsumsplitsn  15717  incexclem  15809  supcvg  15829  mertenslem2  15858  fprodn0  15952  fprodsplitsn  15962  fprodle  15969  eftlcl  16082  reeftlcl  16083  rpnnen2lem6  16194  dvdsext  16298  3dvds  16308  sqoddm1div8z  16331  gcdcllem3  16478  dvdsexpim  16532  bezoutr1  16546  seq1st  16548  dvdslcm  16575  lcmeq0  16577  lcmcl  16578  lcmneg  16580  lcmdvds  16585  coprmgcdb  16626  dvdsprime  16664  pc2dvds  16857  prmpwdvds  16882  unbenlem  16886  infpnlem1  16888  1arith  16905  vdwmc2  16957  ramcl  17007  mrcuni  17589  isacs1i  17625  acsfn  17627  funcpropd  17871  curfcl  18200  curf2ndf  18215  resmgmhm  18645  resmgmhm2b  18647  mgmhmco  18648  mgmhmima  18649  resmhm  18754  resmhm2b  18756  mhmco  18757  pwsdiagmhm  18765  gsumwsubmcl  18771  gsumwspan  18780  pwmnd  18871  dfgrp2  18901  subgint  19089  ghmmhmb  19166  resghm  19171  cntzmhm  19280  symgextf1lem  19357  f1omvdconj  19383  dfod2  19501  gexdvds  19521  subgpgp  19534  sylow1lem3  19537  frgpnabllem1  19810  dprdfeq0  19961  rhmimasubrnglem  20481  cntzsubrng  20483  cntzsubr  20522  isdrng2  20659  islmodd  20779  lsslss  20874  reslmhm2b  20968  rngqiprngimfo  21218  psgnfix1  21514  psgndif  21518  copsgndif  21519  ocvocv  21587  frlmsslsp  21712  frlmlbs  21713  psrbaglefi  21842  psrdi  21881  psrass23l  21883  psrass23  21885  psdmul  22060  mptcoe1fsupp  22107  psropprmul  22129  ply1coe  22192  rhmcomulmpl  22276  mamudi  22297  mamudir  22298  mat1dimelbas  22365  scmatmulcl  22412  scmatfo  22424  mulmarep1gsum2  22468  mdetunilem7  22512  mdetunilem9  22514  gsummatr01lem3  22551  smadiadetlem3  22562  cpmadugsumlemF  22770  leordtval  23107  cnpnei  23158  cnco  23160  cnss1  23170  cmpsub  23294  hauscmplem  23300  dissnlocfin  23423  ptbasid  23469  tx2cn  23504  upxp  23517  txindis  23528  xkoptsub  23548  xkopt  23549  trfbas2  23737  filconn  23777  trfil2  23781  filssufilg  23805  ufileu  23813  fixufil  23816  ufilen  23824  rnelfmlem  23846  flimclsi  23872  hauspwpwf1  23881  fclsopn  23908  fclsfnflim  23921  fclscmpi  23923  alexsubALTlem4  23944  ptcmplem5  23950  tgpmulg  23987  subgtgp  23999  tgpt0  24013  tsmsxplem2  24048  metss  24403  metustfbas  24452  dscopn  24468  xrsmopn  24708  cncfss  24799  icoopnst  24843  iccpnfcnv  24849  icccvx  24855  evth  24865  phtpycc  24897  pcohtpylem  24926  lmmbrf  25169  fgcfil  25178  caucfil  25190  cfilres  25203  bcth3  25238  cmscsscms  25280  ovolfioo  25375  ovolficc  25376  voliunlem3  25460  volcn  25514  mbflimsup  25574  mbfi1fseqlem5  25627  itg2seq  25650  bddiblnc  25750  dvnff  25832  dvnadd  25838  cpnord  25844  c1liplem1  25908  plypf1  26124  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeidlem  26149  dgrle  26155  dgrnznn  26159  plycjlem  26189  elqaalem3  26236  ulmcaulem  26310  ulmcau  26311  psergf  26328  psercn2  26339  psercn2OLD  26340  efopn  26574  abscxpbnd  26670  leibpi  26859  isppw2  27032  muinv  27110  bposlem3  27204  gausslemma2dlem4  27287  pntrmax  27482  pntpbnd1  27504  qabvexp  27544  madebday  27818  mulsrid  28023  bdayon  28180  peano5n0s  28219  zs12bday  28350  eqeelen  28838  colinearalglem4  28843  axcgrid  28850  axsegconlem1  28851  axsegconlem3  28853  ax5seglem1  28862  ax5seglem2  28863  ax5seglem9  28871  axcontlem2  28899  cusgrfilem2  29391  vtxdgfisf  29411  usgr2pthlem  29700  uspgrn2crct  29745  crctcshwlkn0  29758  wwlksnext  29830  wwlksnextproplem3  29848  eupth2lem3lem4  30167  frgr3vlem1  30209  frgr3vlem2  30210  3vfriswmgrlem  30213  frgrwopreglem5  30257  numclwwlk3lem2  30320  grpoidinvlem3  30442  grpoidinv  30444  grpoideu  30445  nmoub3i  30709  nmlno0lem  30729  nmlnoubi  30732  ipasslem3  30769  ipblnfi  30791  hvaddsub4  31014  his35  31024  shsel3  31251  chj4  31471  spansncol  31504  chscllem2  31574  5oalem2  31591  3oalem2  31599  hoaddcl  31694  adjsym  31769  cnvadj  31828  hhcno  31840  hhcnf  31841  nmopub2tALT  31845  unoplin  31856  counop  31857  nmfnleub2  31862  hmoplin  31878  brafnmul  31887  nmlnop0iALT  31931  nmopun  31950  nmophmi  31967  riesz3i  31998  riesz1  32001  cnlnadjlem2  32004  cnlnadjlem6  32008  adjmul  32028  adjadd  32029  bra11  32044  cnvbraval  32046  kbass5  32056  kbass6  32057  leop2  32060  leopadd  32068  leopmuli  32069  leoptri  32072  leopnmid  32074  nmopleid  32075  pj3si  32143  hstel2  32155  cvcon3  32220  dmdmd  32236  dmdbr5  32244  mdsl0  32246  mdslmd1lem1  32261  mdslmd1lem2  32262  mdslmd3i  32268  superpos  32290  chirredlem2  32327  chirredlem3  32328  mdsymlem3  32341  mdsymlem5  32343  mdsymlem6  32344  sumdmdlem  32354  cdjreui  32368  cdj1i  32369  cdj3i  32377  foresf1o  32440  2ndimaxp  32577  abfmpel  32586  fcomptf  32589  fcnvgreu  32604  fdifsuppconst  32619  xrge0infss  32690  xnn0gt0  32699  sgn3da  32766  cycpm2tr  33083  elrgspnlem2  33201  elrgspnlem3  33202  intlidl  33398  rhmpreimaprmidl  33429  lssdimle  33610  mdetpmtr1  33820  cmpcref  33847  xrge0iifcnv  33930  zrhcntr  33976  esumcst  34060  hasheuni  34082  esum2dlem  34089  esum2d  34090  sigaclcu2  34117  insiga  34134  unelldsys  34155  measres  34219  measdivcst  34221  volfiniune  34227  ddemeas  34233  actfunsnf1o  34602  fnrelpredd  35086  fineqvac  35094  sconnpi1  35233  cvmsss2  35268  satfv1lem  35356  fmlaomn0  35384  gonarlem  35388  mrsubco  35515  dfon2lem6  35783  hfext  36178  elicc3  36312  fnessref  36352  bj-ismooredr2  37105  pibt2  37412  fin2solem  37607  fin2so  37608  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem2  37623  poimirlem14  37635  poimirlem25  37646  poimirlem26  37647  poimirlem29  37650  poimirlem30  37651  broucube  37655  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ex-ovoliunnfl  37664  mbfresfi  37667  cnambfre  37669  itg2addnclem  37672  itg2addnclem2  37673  itg2addnc  37675  ftc1anclem3  37696  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  indexdom  37735  filbcmb  37741  fdc  37746  incsequz  37749  metf1o  37756  caures  37761  bndss  37787  ismtycnv  37803  heiborlem1  37812  rrncmslem  37833  isdrngo2  37959  rngoisocnv  37982  unichnidl  38032  erimeq2  38677  ax12eq  38941  ax12el  38942  lshpset2N  39119  pmapglb2N  39772  pmapglb2xN  39773  pclfinN  39901  polval2N  39907  cdleme31fv2  40394  cdleme32fvcl  40441  cdleme48gfv  40538  tendoicl  40797  tendoipl  40798  diaglbN  41056  dochkr1  41479  dochkr1OLDN  41480  sumcubes  42308  expeq1d  42319  zaddcomlem  42458  zmulcomlem  42462  fiabv  42531  rhmcomulpsr  42546  evlsvvval  42558  selvcllem5  42577  evlselv  42582  fsuppind  42585  fsuppssind  42588  mhpind  42589  nacsfix  42707  eq0rabdioph  42771  diophren  42808  rencldnfilem  42815  pell1234qrdich  42856  jm2.24  42959  jm2.26lem3  42997  wepwsolem  43038  pwssplit4  43085  isnumbasgrplem3  43101  onexoegt  43240  onov0suclim  43270  cantnfresb  43320  omcl2  43329  ofoaid1  43354  ofoaid2  43355  grumnudlem  44281  cvgdvgrat  44309  ofsubid  44320  bcc0  44336  binomcxplemnn0  44345  uzwo4  45054  fiiuncl  45066  iunincfi  45095  nsstr  45096  rexanuz3  45097  iinssiin  45130  disjrnmpt2  45189  disjinfi  45193  choicefi  45201  fsneq  45207  difmap  45208  iunmapsn  45218  axccdom  45223  axccd  45230  rnmptlb  45244  rnmptbd2lem  45249  ssfiunibd  45314  supxrgelem  45340  suplesup  45342  xrlexaddrp  45355  xralrple2  45357  infxrunb2  45371  xralrple3  45377  xrralrecnnle  45386  xrralrecnnge  45393  supxrunb3  45402  unb2ltle  45418  rexabslelem  45421  supminfrnmpt  45448  infxrpnf  45449  supminfxr  45467  supminfxr2  45472  xrpnf  45488  pimxrneun  45491  cvgcaule  45494  iooiinicc  45547  ressioosup  45560  iooiinioc  45561  ressiooinf  45562  fsumsupp0  45583  divcnvg  45632  limcrecl  45634  sumnnodd  45635  islpcn  45644  lptre2pt  45645  limcresiooub  45647  limcresioolb  45648  limclner  45656  fnlimfvre  45679  allbutfifvre  45680  climinf3  45721  limsupmnflem  45725  limsupre3uzlem  45740  limsupreuzmpt  45744  climuzlem  45748  climisp  45751  climrescn  45753  climxrrelem  45754  climxrre  45755  climlimsupcex  45774  liminflelimsuplem  45780  limsupgtlem  45782  liminfvalxr  45788  liminfreuzlem  45807  liminfltlem  45809  liminflimsupclim  45812  xlimpnfxnegmnf  45819  liminflbuz2  45820  liminflimsupxrre  45822  cnrefiisplem  45834  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem2  45842  xlimpnfv  45843  xlimmnfmpt  45848  xlimpnfmpt  45849  climxlim2lem  45850  dfxlim2v  45852  xlimliminflimsup  45867  cncfuni  45891  icccncfext  45892  cncficcgt0  45893  cncfiooicclem1  45898  cncfiooiccre  45900  dvasinbx  45925  dvdsn1add  45944  dvnmul  45948  dvmptfprodlem  45949  dvnprodlem1  45951  dvnprodlem3  45953  iblspltprt  45978  itgioocnicc  45982  itgspltprt  45984  ismbl3  45991  stirlinglem5  46083  dirker2re  46097  dirkerper  46101  dirkertrigeq  46106  dirkercncflem2  46109  fourierdlem12  46124  fourierdlem15  46127  fourierdlem16  46128  fourierdlem20  46132  fourierdlem21  46133  fourierdlem22  46134  fourierdlem39  46151  fourierdlem40  46152  fourierdlem41  46153  fourierdlem42  46154  fourierdlem46  46157  fourierdlem49  46160  fourierdlem50  46161  fourierdlem57  46168  fourierdlem58  46169  fourierdlem59  46170  fourierdlem64  46175  fourierdlem65  46176  fourierdlem66  46177  fourierdlem68  46179  fourierdlem70  46181  fourierdlem71  46182  fourierdlem73  46184  fourierdlem78  46189  fourierdlem79  46190  fourierdlem80  46191  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem87  46198  fourierdlem93  46204  fourierdlem95  46206  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  sqwvfoura  46233  fourierswlem  46235  elaa2lem  46238  etransclem13  46252  etransclem23  46262  etransclem24  46263  etransclem32  46271  etransclem38  46277  etransclem46  46285  qndenserrnbllem  46299  rrxsnicc  46305  ioorrnopnlem  46309  prsal  46323  intsal  46335  salexct  46339  dfsalgen2  46346  issalnnd  46350  sge0rnre  46369  sge0val  46371  sge0z  46380  sge0revalmpt  46383  sge0tsms  46385  sge0pr  46399  sge0resplit  46411  sge0split  46414  sge0splitmpt  46416  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0fodjrnlem  46421  sge0iunmpt  46423  sge0rpcpnf  46426  sge0ltfirpmpt2  46431  sge0isum  46432  sge0xaddlem1  46438  sge0xaddlem2  46439  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0seq  46451  sge0reuz  46452  nnfoctbdjlem  46460  nnfoctbdj  46461  meadjun  46467  meadjiunlem  46470  voliunsge0lem  46477  meaiuninc3v  46489  omeiunltfirp  46524  carageniuncllem2  46527  caratheodorylem1  46531  caratheodorylem2  46532  caratheodory  46533  isomenndlem  46535  isomennd  46536  hoicvr  46553  volicorescl  46558  ovnsubaddlem2  46576  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvle  46605  ovnhoilem2  46607  hspdifhsp  46621  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem2  46632  ovnsubadd2lem  46650  ovolval4lem1  46654  vonvolmbl  46666  vonioo  46687  vonicc  46690  pimrecltpos  46713  issmfle  46750  smflimlem1  46776  smflimlem2  46777  smflimlem6  46781  smfresal  46793  smfrec  46794  smfmullem4  46799  smfpimcc  46813  smflimmpt  46815  smfsuplem1  46816  smfsuplem3  46818  smfsupmpt  46820  smfsupxr  46821  smfinflem  46822  smfinfmpt  46824  smflimsuplem4  46828  smflimsuplem5  46829  smflimsupmpt  46834  smfliminfmpt  46837  fsupdm  46847  finfdm  46851  smonoord  47376  lswn0  47449  poprelb  47529  fmtnoprmfac1  47570  fmtnofac2lem  47573  sbgoldbst  47783  isgrim  47886  gpgedgvtx0  48056  snlindsntorlem  48463  1arymaptf  48634  ipolubdm  48979  ipoglbdm  48982  setc1onsubc  49595  aacllem  49794