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 488	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan 583	1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad2antlr  727  ad2ant2l  746  ad2ant2lr  748  ad5ant23  760  ad5ant24  761  ad5ant25  762  3adant1  1132  3ad2antl3  1189  ralcom2  3265  ralimda  3397  vtocl2d  3462  sbc2iegf  3764  sbcralt  3771  pofun  5471  poinxp  5614  xpdifid  6011  sossfld  6029  predpo  6158  preddowncl  6168  tz7.7  6217  onfr  6230  ssimaex  6774  fndmdif  6840  dffo4  6900  fcompt  6926  fconst2g  6996  f1cofveqaeq  7048  2f1fvneq  7050  isores3  7122  fvmptopab  7244  limsssuc  7607  el2mpocl  7832  1stconst  7846  2ndconst  7847  curry1  7850  curry2  7853  extmptsuppeq  7908  suppss  7914  suppssOLD  7915  suppssov1  7918  suppss2  7920  onnseq  8059  oe0  8227  oesuclem  8230  oecl  8242  oaordi  8252  oawordri  8256  omordi  8272  omword2  8280  omlimcl  8284  odi  8285  omass  8286  oeoe  8305  nnaordi  8324  oaabs  8351  omsmolem  8360  eceqoveq  8482  mapsnd  8545  dom2lem  8646  sbthlem9  8742  php3  8810  onomeneq  8845  isinf  8867  frfi  8894  fiint  8926  fodomfib  8928  fofinf1o  8929  marypha1lem  9027  ordiso2  9109  unwdomg  9178  xpwdomg  9179  dftrpred3g  9317  ac5num  9615  cff1  9837  cfcoflem  9851  infpssrlem4  9885  isf32lem9  9940  isf34lem7  9958  fin1a2lem13  9991  fin1a2s  9993  hsmexlem4  10008  axdc2lem  10027  zorn2lem6  10080  axpowndlem2  10177  inttsk  10353  tskuni  10362  nqereu  10508  prcdnq  10572  addclprlem2  10596  ltexpri  10622  prlem936  10626  reclem2pr  10627  axsup  10873  add4  11017  ltleadd  11280  lt2mul2div  11675  nn2ge  11822  zextle  12215  fnn0ind  12241  xrlttr  12695  ifle  12752  xnn0lem1lt  12799  xaddass  12804  xmulasslem3  12841  xlemul1a  12843  xadddilem  12849  xrsupsslem  12862  xrinfmsslem  12863  supxrunb1  12874  supxrunb2  12875  ixxin  12917  difreicc  13037  iccsplit  13038  iccshftr  13039  iccshftl  13041  iccdil  13043  icccntr  13045  fzaddel  13111  fzadd2  13112  fzrev  13140  modadd1  13446  modmul1  13462  fsuppmapnn0fiub  13529  mulexp  13639  expadd  13642  expmul  13645  expnbnd  13764  bccl  13853  hashdom  13911  prsshashgt1  13942  hashfacen  13983  hashfacenOLD  13984  brfi1uzind  14029  wrdnval  14065  swrdccat3blem  14269  revccat  14296  2shfti  14608  rexico  14882  cau3lem  14883  subcn2  15121  caucvgb  15208  iseraltlem1  15210  sumss  15253  fsumsplitsn  15272  incexclem  15363  supcvg  15383  mertenslem2  15412  fprodn0  15504  fprodsplitsn  15514  fprodle  15521  eftlcl  15631  reeftlcl  15632  rpnnen2lem6  15743  dvdsext  15845  3dvds  15855  sqoddm1div8z  15878  gcdcllem3  16023  bezoutr1  16089  seq1st  16091  dvdslcm  16118  lcmeq0  16120  lcmcl  16121  lcmneg  16123  lcmdvds  16128  coprmgcdb  16169  dvdsprime  16207  pc2dvds  16395  prmpwdvds  16420  unbenlem  16424  infpnlem1  16426  1arith  16443  vdwmc2  16495  ramcl  16545  mrcuni  17078  isacs1i  17114  acsfn  17116  funcpropd  17361  curfcl  17694  curf2ndf  17709  resmhm  18201  resmhm2b  18203  mhmco  18204  mhmima  18205  pwsdiagmhm  18211  gsumwsubmcl  18217  gsumwspan  18227  pwmnd  18318  dfgrp2  18346  subgint  18521  ghmmhmb  18587  resghm  18592  cntzmhm  18687  symgextf1lem  18766  f1omvdconj  18792  dfod2  18909  gexdvds  18927  subgpgp  18940  sylow1lem3  18943  frgpnabllem1  19212  dprdfeq0  19363  isdrng2  19731  cntzsubr  19787  islmodd  19859  lsslss  19952  reslmhm2b  20045  psgnfix1  20514  psgndif  20518  copsgndif  20519  ocvocv  20587  frlmsslsp  20712  frlmlbs  20713  psrbaglefi  20845  psrbaglefiOLD  20846  mptcoe1fsupp  21090  psropprmul  21113  ply1coe  21171  mamudi  21254  mamudir  21255  mat1dimelbas  21322  scmatmulcl  21369  scmatfo  21381  mulmarep1gsum2  21425  mdetunilem7  21469  mdetunilem9  21471  gsummatr01lem3  21508  smadiadetlem3  21519  cpmadugsumlemF  21727  leordtval  22064  cnpnei  22115  cnco  22117  cnss1  22127  cmpsub  22251  hauscmplem  22257  dissnlocfin  22380  ptbasid  22426  tx2cn  22461  upxp  22474  txindis  22485  xkoptsub  22505  xkopt  22506  trfbas2  22694  filconn  22734  trfil2  22738  filssufilg  22762  ufileu  22770  fixufil  22773  ufilen  22781  rnelfmlem  22803  flimclsi  22829  hauspwpwf1  22838  fclsopn  22865  fclsfnflim  22878  fclscmpi  22880  alexsubALTlem4  22901  ptcmplem5  22907  tgpmulg  22944  subgtgp  22956  tgpt0  22970  tsmsxplem2  23005  metss  23360  metustfbas  23409  dscopn  23425  xrsmopn  23663  cncfss  23750  icoopnst  23790  iccpnfcnv  23795  icccvx  23801  evth  23810  phtpycc  23842  pcohtpylem  23870  lmmbrf  24113  fgcfil  24122  caucfil  24134  cfilres  24147  bcth3  24182  cmscsscms  24224  ovolfioo  24318  ovolficc  24319  voliunlem3  24403  volcn  24457  mbflimsup  24517  mbfi1fseqlem5  24571  itg2seq  24594  bddiblnc  24693  dvnff  24774  dvnadd  24780  cpnord  24786  c1liplem1  24847  plypf1  25060  plyaddlem1  25061  plymullem1  25062  coeeulem  25072  coeidlem  25085  dgrle  25091  dgrnznn  25095  plycjlem  25124  elqaalem3  25168  ulmcaulem  25240  ulmcau  25241  psergf  25258  psercn2  25269  efopn  25500  abscxpbnd  25593  leibpi  25779  isppw2  25951  muinv  26029  bposlem3  26121  gausslemma2dlem4  26204  pntrmax  26399  pntpbnd1  26421  qabvexp  26461  eqeelen  26949  colinearalglem4  26954  axcgrid  26961  axsegconlem1  26962  axsegconlem3  26964  ax5seglem1  26973  ax5seglem2  26974  ax5seglem9  26982  axcontlem2  27010  cusgrfilem2  27498  vtxdgfisf  27518  usgr2pthlem  27804  uspgrn2crct  27846  crctcshwlkn0  27859  wwlksnext  27931  wwlksnextproplem3  27949  eupth2lem3lem4  28268  frgr3vlem1  28310  frgr3vlem2  28311  3vfriswmgrlem  28314  frgrwopreglem5  28358  numclwwlk3lem2  28421  grpoidinvlem3  28541  grpoidinv  28543  grpoideu  28544  nmoub3i  28808  nmlno0lem  28828  nmlnoubi  28831  ipasslem3  28868  ipblnfi  28890  hvaddsub4  29113  his35  29123  shsel3  29350  chj4  29570  spansncol  29603  chscllem2  29673  5oalem2  29690  3oalem2  29698  hoaddcl  29793  adjsym  29868  cnvadj  29927  hhcno  29939  hhcnf  29940  nmopub2tALT  29944  unoplin  29955  counop  29956  nmfnleub2  29961  hmoplin  29977  brafnmul  29986  nmlnop0iALT  30030  nmopun  30049  nmophmi  30066  riesz3i  30097  riesz1  30100  cnlnadjlem2  30103  cnlnadjlem6  30107  adjmul  30127  adjadd  30128  bra11  30143  cnvbraval  30145  kbass5  30155  kbass6  30156  leop2  30159  leopadd  30167  leopmuli  30168  leoptri  30171  leopnmid  30173  nmopleid  30174  pj3si  30242  hstel2  30254  cvcon3  30319  dmdmd  30335  dmdbr5  30343  mdsl0  30345  mdslmd1lem1  30360  mdslmd1lem2  30361  mdslmd3i  30367  superpos  30389  chirredlem2  30426  chirredlem3  30427  mdsymlem3  30440  mdsymlem5  30442  mdsymlem6  30443  sumdmdlem  30453  cdjreui  30467  cdj1i  30468  cdj3i  30476  foresf1o  30523  2ndimaxp  30657  abfmpel  30666  fcomptf  30669  fcnvgreu  30684  fdifsuppconst  30697  xrge0infss  30757  xnn0gt0  30766  cycpm2tr  31059  intlidl  31270  rhmpreimaprmidl  31295  lssdimle  31359  mdetpmtr1  31441  cmpcref  31468  xrge0iifcnv  31551  esumcst  31697  hasheuni  31719  esum2dlem  31726  esum2d  31727  sigaclcu2  31754  insiga  31771  unelldsys  31792  measres  31856  measdivcst  31858  volfiniune  31864  ddemeas  31870  sgn3da  32174  actfunsnf1o  32250  fnrelpredd  32728  fineqvac  32733  sconnpi1  32868  cvmsss2  32903  satfv1lem  32991  fmlaomn0  33019  gonarlem  33023  mrsubco  33150  dfon2lem6  33434  poseq  33482  soseq  33483  frr1  33507  madebday  33766  hfext  34171  elicc3  34192  fnessref  34232  bj-ismooredr2  34965  pibt2  35274  fin2solem  35449  fin2so  35450  lindsenlbs  35458  matunitlindflem1  35459  matunitlindflem2  35460  poimirlem2  35465  poimirlem14  35477  poimirlem25  35488  poimirlem26  35489  poimirlem29  35492  poimirlem30  35493  broucube  35497  heicant  35498  mblfinlem2  35501  mblfinlem3  35502  mblfinlem4  35503  ex-ovoliunnfl  35506  mbfresfi  35509  cnambfre  35511  itg2addnclem  35514  itg2addnclem2  35515  itg2addnc  35517  ftc1anclem3  35538  ftc1anclem4  35539  ftc1anclem5  35540  ftc1anclem6  35541  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  eqfnun  35566  indexdom  35578  filbcmb  35584  fdc  35589  incsequz  35592  metf1o  35599  caures  35604  bndss  35630  ismtycnv  35646  heiborlem1  35655  rrncmslem  35676  isdrngo2  35802  rngoisocnv  35825  unichnidl  35875  erim2  36475  ax12eq  36641  ax12el  36642  lshpset2N  36819  pmapglb2N  37471  pmapglb2xN  37472  pclfinN  37600  polval2N  37606  cdleme31fv2  38093  cdleme32fvcl  38140  cdleme48gfv  38237  tendoicl  38496  tendoipl  38497  diaglbN  38755  dochkr1  39178  dochkr1OLDN  39179  selvval2lem5  39883  fsuppind  39930  fsuppssind  39933  mhpind  39934  dvdsexpim  39977  nacsfix  40178  eq0rabdioph  40242  diophren  40279  rencldnfilem  40286  pell1234qrdich  40327  jm2.24  40429  jm2.26lem3  40467  wepwsolem  40511  pwssplit4  40558  isnumbasgrplem3  40574  grumnudlem  41517  cvgdvgrat  41545  ofsubid  41556  bcc0  41572  binomcxplemnn0  41581  uzwo4  42215  fiiuncl  42227  iunincfi  42258  nsstr  42259  rexanuz3  42260  iinssiin  42292  disjrnmpt2  42340  fompt  42344  disjinfi  42345  choicefi  42354  fsneq  42360  difmap  42361  iunmapsn  42371  axccdom  42376  axccd  42382  rnmptlb  42401  rnmptbd2lem  42407  ssfiunibd  42462  supxrgelem  42490  suplesup  42492  xrlexaddrp  42505  xralrple2  42507  infxrunb2  42521  xralrple3  42527  xrralrecnnle  42536  xrralrecnnge  42544  supxrunb3  42553  unb2ltle  42569  rexabslelem  42572  supminfrnmpt  42599  infxrpnf  42601  supminfxr  42620  supminfxr2  42625  xrpnf  42642  iooiinicc  42696  ressioosup  42709  iooiinioc  42710  ressiooinf  42711  fsumsupp0  42737  divcnvg  42786  limcrecl  42788  sumnnodd  42789  islpcn  42798  lptre2pt  42799  limcresiooub  42801  limcresioolb  42802  limclner  42810  fnlimfvre  42833  allbutfifvre  42834  climinf3  42875  limsupmnflem  42879  limsupre3uzlem  42894  limsupreuzmpt  42898  climuzlem  42902  climisp  42905  climrescn  42907  climxrrelem  42908  climxrre  42909  climlimsupcex  42928  liminflelimsuplem  42934  limsupgtlem  42936  liminfvalxr  42942  liminfreuzlem  42961  liminfltlem  42963  liminflimsupclim  42966  xlimpnfxnegmnf  42973  liminflbuz2  42974  liminflimsupxrre  42976  cnrefiisplem  42988  xlimmnfvlem2  42992  xlimmnfv  42993  xlimpnfvlem2  42996  xlimpnfv  42997  xlimmnfmpt  43002  xlimpnfmpt  43003  climxlim2lem  43004  dfxlim2v  43006  xlimliminflimsup  43021  cncfuni  43045  icccncfext  43046  cncficcgt0  43047  cncfiooicclem1  43052  cncfiooiccre  43054  dvasinbx  43079  dvdsn1add  43098  dvnmul  43102  dvmptfprodlem  43103  dvnprodlem1  43105  dvnprodlem3  43107  iblspltprt  43132  itgioocnicc  43136  itgspltprt  43138  ismbl3  43145  stirlinglem5  43237  dirker2re  43251  dirkerper  43255  dirkertrigeq  43260  dirkercncflem2  43263  fourierdlem12  43278  fourierdlem15  43281  fourierdlem16  43282  fourierdlem20  43286  fourierdlem21  43287  fourierdlem22  43288  fourierdlem39  43305  fourierdlem40  43306  fourierdlem41  43307  fourierdlem42  43308  fourierdlem46  43311  fourierdlem49  43314  fourierdlem50  43315  fourierdlem57  43322  fourierdlem58  43323  fourierdlem59  43324  fourierdlem64  43329  fourierdlem65  43330  fourierdlem66  43331  fourierdlem68  43333  fourierdlem70  43335  fourierdlem71  43336  fourierdlem73  43338  fourierdlem78  43343  fourierdlem79  43344  fourierdlem80  43345  fourierdlem81  43346  fourierdlem82  43347  fourierdlem83  43348  fourierdlem87  43352  fourierdlem93  43358  fourierdlem95  43360  fourierdlem101  43366  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  fourierdlem112  43377  sqwvfoura  43387  fourierswlem  43389  elaa2lem  43392  etransclem13  43406  etransclem23  43416  etransclem24  43417  etransclem32  43425  etransclem38  43431  etransclem46  43439  qndenserrnbllem  43453  rrxsnicc  43459  ioorrnopnlem  43463  prsal  43477  intsal  43487  salexct  43491  dfsalgen2  43498  issalnnd  43502  sge0rnre  43520  sge0val  43522  sge0z  43531  sge0revalmpt  43534  sge0tsms  43536  sge0pr  43550  sge0resplit  43562  sge0split  43565  sge0splitmpt  43567  sge0iunmptlemfi  43569  sge0iunmptlemre  43571  sge0fodjrnlem  43572  sge0iunmpt  43574  sge0rpcpnf  43577  sge0ltfirpmpt2  43582  sge0isum  43583  sge0xaddlem1  43589  sge0xaddlem2  43590  sge0pnffsumgt  43598  sge0gtfsumgt  43599  sge0seq  43602  sge0reuz  43603  nnfoctbdjlem  43611  nnfoctbdj  43612  meadjun  43618  meadjiunlem  43621  voliunsge0lem  43628  meaiuninc3v  43640  omeiunltfirp  43675  carageniuncllem2  43678  caratheodorylem1  43682  caratheodorylem2  43683  caratheodory  43684  isomenndlem  43686  isomennd  43687  hoicvr  43704  volicorescl  43709  ovnsubaddlem2  43727  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvle  43756  ovnhoilem2  43758  hspdifhsp  43772  hoiqssbllem2  43779  hoiqssbllem3  43780  hspmbllem2  43783  ovnsubadd2lem  43801  ovolval4lem1  43805  vonvolmbl  43817  vonioo  43838  vonicc  43841  pimrecltpos  43861  issmfle  43896  smflimlem1  43921  smflimlem2  43922  smflimlem6  43926  smfresal  43937  smfrec  43938  smfmullem4  43943  smfpimcc  43956  smflimmpt  43958  smfsuplem1  43959  smfsuplem3  43961  smfsupmpt  43963  smfsupxr  43964  smfinflem  43965  smfinfmpt  43967  smflimsuplem4  43971  smflimsuplem5  43972  smflimsupmpt  43977  smfliminfmpt  43980  smonoord  44439  lswn0  44512  poprelb  44592  fmtnoprmfac1  44633  fmtnofac2lem  44636  sbgoldbst  44846  resmgmhm  44968  resmgmhm2b  44970  mgmhmco  44971  mgmhmima  44972  snlindsntorlem  45427  1arymaptf  45603  ipolubdm  45889  ipoglbdm  45892  aacllem  46119