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  760  ad5ant24  761  ad5ant25  762  3adant1  1129  3ad2antl3  1186  ralcom2  3374  vtocl2d  3561  sbc2iegf  3872  sbcralt  3880  pofun  5614  poinxp  5768  xpdifid  6189  sossfld  6207  preddowncl  6354  tz7.7  6411  onfr  6424  ssimaex  6993  eqfnun  7056  fndmdif  7061  dffo4  7122  fompt  7137  fcompt  7152  fconst2g  7222  f1cofveqaeq  7277  2f1fvneq  7279  isores3  7354  fvmptopabOLD  7487  limsssuc  7870  el2mpocl  8109  1stconst  8123  2ndconst  8124  curry1  8127  curry2  8130  poseq  8181  soseq  8182  extmptsuppeq  8211  suppss  8217  suppss2  8223  onnseq  8382  oe0  8558  oesuclem  8561  oecl  8573  oaordi  8582  oawordri  8586  omordi  8602  omword2  8610  omlimcl  8614  odi  8615  omass  8616  oeoe  8635  nnaordi  8654  oaabs  8684  omsmolem  8693  eceqoveq  8860  mapsnd  8924  dom2lem  9030  sbthlem9  9129  rexdif1en  9196  php3OLD  9258  onomeneqOLD  9263  isinf  9293  isinfOLD  9294  frfi  9318  fiint  9363  fiintOLD  9364  fodomfib  9366  fodomfibOLD  9368  fofinf1o  9369  marypha1lem  9470  ordiso2  9552  unwdomg  9621  xpwdomg  9622  frr1  9796  ac5num  10073  cff1  10295  cfcoflem  10309  infpssrlem4  10343  isf32lem9  10398  isf34lem7  10416  fin1a2lem13  10449  fin1a2s  10451  hsmexlem4  10466  axdc2lem  10485  zorn2lem6  10538  axpowndlem2  10635  inttsk  10811  tskuni  10820  nqereu  10966  prcdnq  11030  addclprlem2  11054  ltexpri  11080  prlem936  11084  reclem2pr  11085  axsup  11333  add4  11479  ltleadd  11743  lt2mul2div  12143  nn2ge  12290  zextle  12688  fnn0ind  12714  xrlttr  13178  ifle  13235  xnn0lem1lt  13282  xaddass  13287  xmulasslem3  13324  xlemul1a  13326  xadddilem  13332  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  supxrunb2  13358  ixxin  13400  difreicc  13520  iccsplit  13521  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  fzaddel  13594  fzadd2  13595  fzrev  13623  modadd1  13944  modmul1  13961  fsuppmapnn0fiub  14028  mulexp  14138  expadd  14141  expmul  14144  expnbnd  14267  bccl  14357  hashdom  14414  prsshashgt1  14445  hashfacen  14489  brfi1uzind  14543  wrdnval  14579  swrdccat3blem  14773  revccat  14800  2shfti  15115  rexico  15388  cau3lem  15389  subcn2  15627  caucvgb  15712  iseraltlem1  15714  sumss  15756  fsumsplitsn  15776  incexclem  15868  supcvg  15888  mertenslem2  15917  fprodn0  16011  fprodsplitsn  16021  fprodle  16028  eftlcl  16139  reeftlcl  16140  rpnnen2lem6  16251  dvdsext  16354  3dvds  16364  sqoddm1div8z  16387  gcdcllem3  16534  dvdsexpim  16588  bezoutr1  16602  seq1st  16604  dvdslcm  16631  lcmeq0  16633  lcmcl  16634  lcmneg  16636  lcmdvds  16641  coprmgcdb  16682  dvdsprime  16720  pc2dvds  16912  prmpwdvds  16937  unbenlem  16941  infpnlem1  16943  1arith  16960  vdwmc2  17012  ramcl  17062  mrcuni  17665  isacs1i  17701  acsfn  17703  funcpropd  17953  curfcl  18288  curf2ndf  18303  resmgmhm  18736  resmgmhm2b  18738  mgmhmco  18739  mgmhmima  18740  resmhm  18845  resmhm2b  18847  mhmco  18848  pwsdiagmhm  18856  gsumwsubmcl  18862  gsumwspan  18871  pwmnd  18962  dfgrp2  18992  subgint  19180  ghmmhmb  19257  resghm  19262  cntzmhm  19371  symgextf1lem  19452  f1omvdconj  19478  dfod2  19596  gexdvds  19616  subgpgp  19629  sylow1lem3  19632  frgpnabllem1  19905  dprdfeq0  20056  rhmimasubrnglem  20581  cntzsubrng  20583  cntzsubr  20622  isdrng2  20759  islmodd  20880  lsslss  20976  reslmhm2b  21070  rngqiprngimfo  21328  psgnfix1  21633  psgndif  21637  copsgndif  21638  ocvocv  21706  frlmsslsp  21833  frlmlbs  21834  psrbaglefi  21963  psrdi  22002  psrass23l  22004  psrass23  22006  psdmul  22187  mptcoe1fsupp  22232  psropprmul  22254  ply1coe  22317  rhmcomulmpl  22401  mamudi  22422  mamudir  22423  mat1dimelbas  22492  scmatmulcl  22539  scmatfo  22551  mulmarep1gsum2  22595  mdetunilem7  22639  mdetunilem9  22641  gsummatr01lem3  22678  smadiadetlem3  22689  cpmadugsumlemF  22897  leordtval  23236  cnpnei  23287  cnco  23289  cnss1  23299  cmpsub  23423  hauscmplem  23429  dissnlocfin  23552  ptbasid  23598  tx2cn  23633  upxp  23646  txindis  23657  xkoptsub  23677  xkopt  23678  trfbas2  23866  filconn  23906  trfil2  23910  filssufilg  23934  ufileu  23942  fixufil  23945  ufilen  23953  rnelfmlem  23975  flimclsi  24001  hauspwpwf1  24010  fclsopn  24037  fclsfnflim  24050  fclscmpi  24052  alexsubALTlem4  24073  ptcmplem5  24079  tgpmulg  24116  subgtgp  24128  tgpt0  24142  tsmsxplem2  24177  metss  24536  metustfbas  24585  dscopn  24601  xrsmopn  24847  cncfss  24938  icoopnst  24982  iccpnfcnv  24988  icccvx  24994  evth  25004  phtpycc  25036  pcohtpylem  25065  lmmbrf  25309  fgcfil  25318  caucfil  25330  cfilres  25343  bcth3  25378  cmscsscms  25420  ovolfioo  25515  ovolficc  25516  voliunlem3  25600  volcn  25654  mbflimsup  25714  mbfi1fseqlem5  25768  itg2seq  25791  bddiblnc  25891  dvnff  25973  dvnadd  25979  cpnord  25985  c1liplem1  26049  plypf1  26265  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeidlem  26290  dgrle  26296  dgrnznn  26300  plycjlem  26330  elqaalem3  26377  ulmcaulem  26451  ulmcau  26452  psergf  26469  psercn2  26480  psercn2OLD  26481  efopn  26714  abscxpbnd  26810  leibpi  26999  isppw2  27172  muinv  27250  bposlem3  27344  gausslemma2dlem4  27427  pntrmax  27622  pntpbnd1  27644  qabvexp  27684  madebday  27952  mulsrid  28153  peano5n0s  28338  zs12bday  28438  eqeelen  28933  colinearalglem4  28938  axcgrid  28945  axsegconlem1  28946  axsegconlem3  28948  ax5seglem1  28957  ax5seglem2  28958  ax5seglem9  28966  axcontlem2  28994  cusgrfilem2  29488  vtxdgfisf  29508  usgr2pthlem  29795  uspgrn2crct  29837  crctcshwlkn0  29850  wwlksnext  29922  wwlksnextproplem3  29940  eupth2lem3lem4  30259  frgr3vlem1  30301  frgr3vlem2  30302  3vfriswmgrlem  30305  frgrwopreglem5  30349  numclwwlk3lem2  30412  grpoidinvlem3  30534  grpoidinv  30536  grpoideu  30537  nmoub3i  30801  nmlno0lem  30821  nmlnoubi  30824  ipasslem3  30861  ipblnfi  30883  hvaddsub4  31106  his35  31116  shsel3  31343  chj4  31563  spansncol  31596  chscllem2  31666  5oalem2  31683  3oalem2  31691  hoaddcl  31786  adjsym  31861  cnvadj  31920  hhcno  31932  hhcnf  31933  nmopub2tALT  31937  unoplin  31948  counop  31949  nmfnleub2  31954  hmoplin  31970  brafnmul  31979  nmlnop0iALT  32023  nmopun  32042  nmophmi  32059  riesz3i  32090  riesz1  32093  cnlnadjlem2  32096  cnlnadjlem6  32100  adjmul  32120  adjadd  32121  bra11  32136  cnvbraval  32138  kbass5  32148  kbass6  32149  leop2  32152  leopadd  32160  leopmuli  32161  leoptri  32164  leopnmid  32166  nmopleid  32167  pj3si  32235  hstel2  32247  cvcon3  32312  dmdmd  32328  dmdbr5  32336  mdsl0  32338  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd3i  32360  superpos  32382  chirredlem2  32419  chirredlem3  32420  mdsymlem3  32433  mdsymlem5  32435  mdsymlem6  32436  sumdmdlem  32446  cdjreui  32460  cdj1i  32461  cdj3i  32469  foresf1o  32531  2ndimaxp  32662  abfmpel  32671  fcomptf  32674  fcnvgreu  32689  fdifsuppconst  32703  xrge0infss  32770  xnn0gt0  32779  cycpm2tr  33121  elrgspnlem2  33232  elrgspnlem3  33233  intlidl  33427  rhmpreimaprmidl  33458  lssdimle  33634  mdetpmtr1  33783  cmpcref  33810  xrge0iifcnv  33893  zrhcntr  33941  esumcst  34043  hasheuni  34065  esum2dlem  34072  esum2d  34073  sigaclcu2  34100  insiga  34117  unelldsys  34138  measres  34202  measdivcst  34204  volfiniune  34210  ddemeas  34216  sgn3da  34522  actfunsnf1o  34597  fnrelpredd  35081  fineqvac  35089  sconnpi1  35223  cvmsss2  35258  satfv1lem  35346  fmlaomn0  35374  gonarlem  35378  mrsubco  35505  dfon2lem6  35769  hfext  36164  elicc3  36299  fnessref  36339  bj-ismooredr2  37092  pibt2  37399  fin2solem  37592  fin2so  37593  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem2  37608  poimirlem14  37620  poimirlem25  37631  poimirlem26  37632  poimirlem29  37635  poimirlem30  37636  broucube  37640  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ex-ovoliunnfl  37649  mbfresfi  37652  cnambfre  37654  itg2addnclem  37657  itg2addnclem2  37658  itg2addnc  37660  ftc1anclem3  37681  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  indexdom  37720  filbcmb  37726  fdc  37731  incsequz  37734  metf1o  37741  caures  37746  bndss  37772  ismtycnv  37788  heiborlem1  37797  rrncmslem  37818  isdrngo2  37944  rngoisocnv  37967  unichnidl  38017  erimeq2  38659  ax12eq  38922  ax12el  38923  lshpset2N  39100  pmapglb2N  39753  pmapglb2xN  39754  pclfinN  39882  polval2N  39888  cdleme31fv2  40375  cdleme32fvcl  40422  cdleme48gfv  40519  tendoicl  40778  tendoipl  40779  diaglbN  41037  dochkr1  41460  dochkr1OLDN  41461  sumcubes  42325  expeq1d  42337  zaddcomlem  42457  zmulcomlem  42461  fiabv  42522  rhmcomulpsr  42537  evlsvvval  42549  selvcllem5  42568  evlselv  42573  fsuppind  42576  fsuppssind  42579  mhpind  42580  nacsfix  42699  eq0rabdioph  42763  diophren  42800  rencldnfilem  42807  pell1234qrdich  42848  jm2.24  42951  jm2.26lem3  42989  wepwsolem  43030  pwssplit4  43077  isnumbasgrplem3  43093  onexoegt  43232  onov0suclim  43263  cantnfresb  43313  omcl2  43322  ofoaid1  43347  ofoaid2  43348  grumnudlem  44280  cvgdvgrat  44308  ofsubid  44319  bcc0  44335  binomcxplemnn0  44344  uzwo4  44992  fiiuncl  45004  iunincfi  45033  nsstr  45034  rexanuz3  45035  iinssiin  45068  disjrnmpt2  45130  disjinfi  45134  choicefi  45142  fsneq  45148  difmap  45149  iunmapsn  45159  axccdom  45164  axccd  45171  rnmptlb  45187  rnmptbd2lem  45192  ssfiunibd  45259  supxrgelem  45286  suplesup  45288  xrlexaddrp  45301  xralrple2  45303  infxrunb2  45317  xralrple3  45323  xrralrecnnle  45332  xrralrecnnge  45339  supxrunb3  45348  unb2ltle  45364  rexabslelem  45367  supminfrnmpt  45394  infxrpnf  45395  supminfxr  45413  supminfxr2  45418  xrpnf  45435  pimxrneun  45438  cvgcaule  45441  iooiinicc  45494  ressioosup  45507  iooiinioc  45508  ressiooinf  45509  fsumsupp0  45533  divcnvg  45582  limcrecl  45584  sumnnodd  45585  islpcn  45594  lptre2pt  45595  limcresiooub  45597  limcresioolb  45598  limclner  45606  fnlimfvre  45629  allbutfifvre  45630  climinf3  45671  limsupmnflem  45675  limsupre3uzlem  45690  limsupreuzmpt  45694  climuzlem  45698  climisp  45701  climrescn  45703  climxrrelem  45704  climxrre  45705  climlimsupcex  45724  liminflelimsuplem  45730  limsupgtlem  45732  liminfvalxr  45738  liminfreuzlem  45757  liminfltlem  45759  liminflimsupclim  45762  xlimpnfxnegmnf  45769  liminflbuz2  45770  liminflimsupxrre  45772  cnrefiisplem  45784  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  xlimmnfmpt  45798  xlimpnfmpt  45799  climxlim2lem  45800  dfxlim2v  45802  xlimliminflimsup  45817  cncfuni  45841  icccncfext  45842  cncficcgt0  45843  cncfiooicclem1  45848  cncfiooiccre  45850  dvasinbx  45875  dvdsn1add  45894  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem1  45901  dvnprodlem3  45903  iblspltprt  45928  itgioocnicc  45932  itgspltprt  45934  ismbl3  45941  stirlinglem5  46033  dirker2re  46047  dirkerper  46051  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem12  46074  fourierdlem15  46077  fourierdlem16  46078  fourierdlem20  46082  fourierdlem21  46083  fourierdlem22  46084  fourierdlem39  46101  fourierdlem40  46102  fourierdlem41  46103  fourierdlem42  46104  fourierdlem46  46107  fourierdlem49  46110  fourierdlem50  46111  fourierdlem57  46118  fourierdlem58  46119  fourierdlem59  46120  fourierdlem64  46125  fourierdlem65  46126  fourierdlem66  46127  fourierdlem68  46129  fourierdlem70  46131  fourierdlem71  46132  fourierdlem73  46134  fourierdlem78  46139  fourierdlem79  46140  fourierdlem80  46141  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem87  46148  fourierdlem93  46154  fourierdlem95  46156  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  sqwvfoura  46183  fourierswlem  46185  elaa2lem  46188  etransclem13  46202  etransclem23  46212  etransclem24  46213  etransclem32  46221  etransclem38  46227  etransclem46  46235  qndenserrnbllem  46249  rrxsnicc  46255  ioorrnopnlem  46259  prsal  46273  intsal  46285  salexct  46289  dfsalgen2  46296  issalnnd  46300  sge0rnre  46319  sge0val  46321  sge0z  46330  sge0revalmpt  46333  sge0tsms  46335  sge0pr  46349  sge0resplit  46361  sge0split  46364  sge0splitmpt  46366  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0fodjrnlem  46371  sge0iunmpt  46373  sge0rpcpnf  46376  sge0ltfirpmpt2  46381  sge0isum  46382  sge0xaddlem1  46388  sge0xaddlem2  46389  sge0pnffsumgt  46397  sge0gtfsumgt  46398  sge0seq  46401  sge0reuz  46402  nnfoctbdjlem  46410  nnfoctbdj  46411  meadjun  46417  meadjiunlem  46420  voliunsge0lem  46427  meaiuninc3v  46439  omeiunltfirp  46474  carageniuncllem2  46477  caratheodorylem1  46481  caratheodorylem2  46482  caratheodory  46483  isomenndlem  46485  isomennd  46486  hoicvr  46503  volicorescl  46508  ovnsubaddlem2  46526  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvle  46555  ovnhoilem2  46557  hspdifhsp  46571  hoiqssbllem2  46578  hoiqssbllem3  46579  hspmbllem2  46582  ovnsubadd2lem  46600  ovolval4lem1  46604  vonvolmbl  46616  vonioo  46637  vonicc  46640  pimrecltpos  46663  issmfle  46700  smflimlem1  46726  smflimlem2  46727  smflimlem6  46731  smfresal  46743  smfrec  46744  smfmullem4  46749  smfpimcc  46763  smflimmpt  46765  smfsuplem1  46766  smfsuplem3  46768  smfsupmpt  46770  smfsupxr  46771  smfinflem  46772  smfinfmpt  46774  smflimsuplem4  46778  smflimsuplem5  46779  smflimsupmpt  46784  smfliminfmpt  46787  fsupdm  46797  finfdm  46801  smonoord  47295  lswn0  47368  poprelb  47448  fmtnoprmfac1  47489  fmtnofac2lem  47492  sbgoldbst  47702  isgrim  47805  gpgedgvtx0  47953  snlindsntorlem  48315  1arymaptf  48490  ipolubdm  48775  ipoglbdm  48778  aacllem  49031