Theorem adantll 727

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2antlr  740  ad2ant2l  759  ad2ant2lr  761  ad5ant23  772  ad5ant24  773  ad5ant25  774  3adant1  1148  3ad2antl3  1206  ralcom2  3366  vtocl2d  3527  sbc2iegf  3817  sbcralt  3823  pofun  5584  poinxp  5740  xpdifid  6177  xpdifcnvepel  6178  sossfld  6196  preddowncl  6361  tz7.7  6414  onfr  6428  ssimaex  7001  fsneq  7065  eqfnun  7067  fndmdif  7072  dffo4  7135  fompt  7150  fcompt  7166  fconst2g  7240  f1cofveqaeq  7292  isores3  7374  limsssuc  7895  el2mpocl  8132  1stconst  8148  2ndconst  8149  curry1  8152  curry2  8155  poseq  8212  soseq  8213  extmptsuppeq  8243  suppss  8249  suppss2  8255  onnseq  8390  oe0  8568  oesuclem  8571  oecl  8583  oaordi  8592  oawordri  8596  omordi  8612  omword2  8620  omlimcl  8624  odi  8625  omass  8626  oeoe  8646  nnaordi  8665  oaabs  8695  omsmolem  8704  eceqoveq  8881  mapsnd  8952  dom2lem  9057  sbthlem9  9152  rexdif1en  9214  isinf  9294  frfi  9314  fiint  9356  fodomfib  9358  fofinf1o  9359  marypha1lem  9462  ordiso2  9546  unwdomg  9615  xpwdomg  9616  frr1  9800  ac5num  10154  cff1  10375  cfcoflem  10389  infpssrlem4  10423  isf32lem9  10478  isf34lem7  10496  fin1a2lem13  10529  fin1a2s  10531  hsmexlem4  10546  axdc2lem  10565  zorn2lem6  10618  axpowndlem2  10722  inttsk  10898  tskuni  10907  nqereu  11053  prcdnq  11117  addclprlem2  11141  ltexpri  11167  prlem936  11171  reclem2pr  11172  axsup  11424  add4  11570  ltleadd  11839  lt2mul2div  12235  nn2ge  12405  zextle  12812  fnn0ind  12838  xrlttr  13309  ifle  13367  xnn0lem1lt  13414  xaddass  13419  xmulasslem3  13456  xlemul1a  13458  xadddilem  13464  xrsupsslem  13477  xrinfmsslem  13478  supxrunb1  13489  supxrunb2  13490  ixxin  13533  difreicc  13655  iccsplit  13656  iccshftr  13657  iccshftl  13659  iccdil  13661  icccntr  13663  fzaddel  13732  fzadd2  13733  fzrev  13761  modadd1  14088  modmul1  14107  fsuppmapnn0fiub  14174  mulexp  14284  expadd  14287  expmul  14290  expnbnd  14417  bccl  14507  hashdom  14564  prsshashgt1  14596  hashfacen  14640  brfi1uzind  14694  wrdnval  14731  swrdccat3blem  14930  revccat  14957  2shfti  15276  sgn3da  15297  rexico  15565  cau3lem  15566  subcn2  15806  caucvgb  15891  iseraltlem1  15893  sumss  15934  fsumsplitsn  15954  incexclem  16049  supcvg  16069  mertenslem2  16098  fprodn0  16190  fprodsplitsn  16200  fprodle  16207  eftlcl  16319  reeftlcl  16320  rpnnen2lem6  16431  dvdsext  16535  3dvds  16545  sqoddm1div8z  16568  gcdcllem3  16715  dvdsexpim  16772  bezoutr1  16788  seq1st  16790  dvdslcm  16817  lcmeq0  16819  lcmcl  16820  lcmneg  16822  lcmdvds  16827  coprmgcdb  16868  dvdsprime  16906  pc2dvds  17101  prmpwdvds  17126  unbenlem  17130  infpnlem1  17132  1arith  17149  vdwmc2  17201  ramcl  17251  mrcuni  17845  isacs1i  17881  acsfn  17883  funcpropd  18127  curfcl  18456  curf2ndf  18471  mgmidpfod  18907  resmgmhm  18950  resmgmhm2b  18952  mgmhmco  18953  mgmhmima  18954  resmhm  19066  resmhm2b  19068  mhmco  19069  pwsdiagmhm  19077  gsumwsubmcl  19083  gsumwspan  19092  pwmnd  19193  dfgrp2  19223  subgint  19411  ghmmhmb  19491  resghm  19496  cntzmhm  19606  symgextf1lem  19685  f1omvdconj  19711  dfod2  19829  gexdvds  19849  subgpgp  19862  sylow1lem3  19865  frgpnabllem1  20138  dprdfeq0  20289  rhmimasubrnglem  20868  cntzsubrng  20870  cntzsubr  20909  isdrng2  21048  isdrng3lem1  21056  islmodd  21192  lsslss  21287  reslmhm2b  21380  rngqiprngimfo  21648  rhmpreimaprmidl  21686  psgnfix1  21959  psgndif  21963  copsgndif  21964  ocvocv  22032  frlmsslsp  22157  frlmlbs  22158  lindsenlbs  22212  psrbaglefi  22289  psrdi  22327  psrass23l  22329  psrass23  22331  evlsvvval  22457  rhmcomulmpl  22488  selvcllem5  22503  psdmul  22542  mptcoe1fsupp  22588  psropprmul  22610  ply1coe  22671  mamudi  22773  mamudir  22774  mat1dimelbas  22841  scmatmulcl  22888  scmatfo  22900  mulmarep1gsum2  22944  mdetunilem7  22988  mdetunilem9  22990  gsummatr01lem3  23027  smadiadetlem3  23038  matunitlindflem1  23049  matunitlindflem2  23050  cpmadugsumlemF  23249  leordtval  23586  cnpnei  23637  cnco  23639  cnss1  23649  cmpsub  23773  hauscmplem  23779  dissnlocfin  23903  ptbasid  23949  tx2cn  23984  upxp  23997  txindis  24008  xkoptsub  24028  xkopt  24029  trfbas2  24217  filconn  24257  trfil2  24261  filssufilg  24285  ufileu  24293  fixufil  24296  ufilen  24304  rnelfmlem  24326  flimclsi  24352  hauspwpwf1  24361  fclsopn  24388  fclsfnflim  24401  fclscmpi  24403  alexsubALTlem4  24424  ptcmplem5  24430  tgpmulg  24467  subgtgp  24479  tgpt0  24493  tsmsxplem2  24528  metss  24882  metustfbas  24931  dscopn  24947  xrsmopn  25187  cncfss  25275  icoopnst  25315  iccpnfcnv  25320  icccvx  25326  evth  25335  phtpycc  25367  pcohtpylem  25395  lmmbrf  25638  fgcfil  25647  caucfil  25659  cfilres  25672  bcth3  25707  cmscsscms  25749  ovolfioo  25843  ovolficc  25844  voliunlem3  25928  volcn  25982  mbflimsup  26042  mbfi1fseqlem5  26095  itg2seq  26118  bddiblnc  26217  dvnff  26298  dvnadd  26304  cpnord  26310  c1liplem1  26371  plypf1  26586  plyaddlem1  26587  plymullem1  26588  coeeulem  26598  coeidlem  26611  dgrle  26617  dgrnznn  26621  plycjlem  26650  elqaalem3  26701  ulmcaulem  26778  ulmcau  26779  psergf  26796  psercn2  26807  efopn  27043  abscxpbnd  27138  leibpi  27327  isppw2  27499  muinv  27577  bposlem3  27670  gausslemma2dlem4  27753  pntrmax  27948  pntpbnd1  27970  qabvexp  28010  madebday  28343  mulsrid  28556  bdayons  28719  peano5n0s  28762  bdaypw2n0bndlem  28906  bdayfinlem  28929  eqeelen  29539  colinearalglem4  29544  axcgrid  29551  axsegconlem1  29552  axsegconlem3  29554  ax5seglem1  29563  ax5seglem2  29564  ax5seglem9  29572  axcontlem2  29600  cusgrfilem2  30094  vtxdgfisf  30114  usgr2pthlem  30406  uspgrn2crct  30454  crctcshwlkn0  30467  wwlksnext  30539  wwlksnextproplem3  30557  eupth2lem3lem4  30889  frgr3vlem1  30931  frgr3vlem2  30932  3vfriswmgrlem  30935  frgrwopreglem5  30979  numclwwlk3lem2  31042  grpoidinvlem3  31165  grpoidinv  31167  grpoideu  31168  nmoub3i  31432  nmlno0lem  31452  nmlnoubi  31455  ipasslem3  31492  ipblnfi  31514  hvaddsub4  31737  his35  31747  shsel3  31974  chj4  32194  spansncol  32227  chscllem2  32297  5oalem2  32314  3oalem2  32322  hoaddcl  32417  adjsym  32492  cnvadj  32551  hhcno  32563  hhcnf  32564  nmopub2tALT  32568  unoplin  32579  counop  32580  nmfnleub2  32585  hmoplin  32601  brafnmul  32610  nmlnop0iALT  32654  nmopun  32673  nmophmi  32690  riesz3i  32721  riesz1  32724  cnlnadjlem2  32727  cnlnadjlem6  32731  adjmul  32751  adjadd  32752  bra11  32767  cnvbraval  32769  kbass5  32779  kbass6  32780  leop2  32783  leopadd  32791  leopmuli  32792  leoptri  32795  leopnmid  32797  nmopleid  32798  pj3si  32866  hstel2  32878  cvcon3  32943  dmdmd  32959  dmdbr5  32967  mdsl0  32969  mdslmd1lem1  32984  mdslmd1lem2  32985  mdslmd3i  32991  superpos  33013  chirredlem2  33050  chirredlem3  33051  mdsymlem3  33064  mdsymlem5  33066  mdsymlem6  33067  sumdmdlem  33077  cdjreui  33091  cdj1i  33092  cdj3i  33100  foresf1o  33199  2ndimaxp  33338  abfmpel  33347  fcomptf  33350  fcnvgreu  33364  fdifsuppconst  33379  xrge0infss  33448  xnn0gt0  33457  weinflb  33637  cycpm2tr  33779  elrgspnlem2  33903  elrgspnlem3  33904  intlidl  34074  mplvrpmga  34288  psrmonmul  34293  esplyfval0  34307  vieta  34323  lssdimle  34351  mdetpmtr1  34566  cmpcref  34593  xrge0iifcnv  34676  zrhcntr  34722  esumcst  34806  hasheuni  34828  esum2dlem  34835  esum2d  34836  sigaclcu2  34863  insiga  34881  unelldsys  34902  measres  34966  measdivcst  34968  volfiniune  34974  ddemeas  34980  actfunsnf1o  35344  fnrelpredd  35845  fineqvac  35925  fineqvnttrclselem1  35930  sconnpi1  36212  cvmsss2  36247  satfv1lem  36335  fmlaomn0  36363  gonarlem  36367  mrsubco  36494  dfon2lem6  36765  hfext  37149  elicc3  37320  fnessref  37360  bj-ismooredr2  38301  pibt2  38608  fin2solem  38797  fin2so  38798  poimirlem2  38808  poimirlem14  38820  poimirlem25  38831  poimirlem26  38832  poimirlem29  38835  poimirlem30  38836  broucube  38840  heicant  38841  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  ex-ovoliunnfl  38849  mbfresfi  38852  cnambfre  38854  itg2addnclem  38857  itg2addnclem2  38858  itg2addnc  38860  ftc1anclem3  38881  ftc1anclem4  38882  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anclem8  38886  ftc1anc  38887  indexdom  38936  filbcmb  38940  fdc  38945  incsequz  38948  metf1o  38955  caures  38960  bndss  38986  ismtycnv  39002  heiborlem1  39011  rrncmslem  39032  isdrngo2  39158  rngoisocnv  39181  unichnidl  39231  erimeq2  39961  ax12eq  40264  ax12el  40265  lshpset2N  40442  pmapglb2N  41094  pmapglb2xN  41095  pclfinN  41223  polval2N  41229  cdleme31fv2  41716  cdleme32fvcl  41763  cdleme48gfv  41860  tendoicl  42119  tendoipl  42120  diaglbN  42378  dochkr1  42801  dochkr1OLDN  42802  sumcubes  43636  expeq1d  43647  zaddcomlem  43793  zmulcomlem  43797  fiabv  43866  rhmcomulpsr  43876  evlselv  43883  fsuppind  43884  fsuppssind  43887  mhpind  43888  nacsfix  43989  eq0rabdioph  44053  diophren  44086  rencldnfilem  44093  pell1234qrdich  44134  jm2.24  44236  jm2.26lem3  44274  wepwsolem  44315  pwssplit4  44357  isnumbasgrplem3  44372  onexoegt  44507  onov0suclim  44537  cantnfresb  44587  omcl2  44596  ofoaid1  44621  ofoaid2  44622  grumnudlem  45530  cvgdvgrat  45558  ofsubid  45569  bcc0  45585  binomcxplemnn0  45594  uzwo4  46344  fiiuncl  46356  iunincfi  46382  nsstr  46383  rexanuz3  46384  iinssiin  46417  disjrnmpt2  46476  disjinfi  46480  choicefi  46487  difmap  46493  iunmapsn  46503  axccdom  46508  axccd  46514  rnmptlb  46528  rnmptbd2lem  46533  ssfiunibd  46598  supxrgelem  46622  suplesup  46624  xrlexaddrp  46637  xralrple2  46639  infxrunb2  46652  xralrple3  46658  xrralrecnnle  46667  xrralrecnnge  46674  supxrunb3  46683  unb2ltle  46698  rexabslelem  46701  supminfrnmpt  46728  infxrpnf  46729  supminfxr  46747  supminfxr2  46752  xrpnf  46768  pimxrneun  46771  cvgcaule  46774  iooiinicc  46827  ressioosup  46840  iooiinioc  46841  ressiooinf  46842  fsumsupp0  46863  divcnvg  46912  limcrecl  46914  sumnnodd  46915  islpcn  46922  lptre2pt  46923  limcresiooub  46925  limcresioolb  46926  limclner  46934  fnlimfvre  46957  allbutfifvre  46958  climinf3  46999  limsupmnflem  47003  limsupre3uzlem  47018  limsupreuzmpt  47022  climuzlem  47026  climisp  47029  climrescn  47031  climxrrelem  47032  climxrre  47033  climlimsupcex  47052  liminflelimsuplem  47058  limsupgtlem  47060  liminfvalxr  47066  liminfreuzlem  47085  liminfltlem  47087  liminflimsupclim  47090  xlimpnfxnegmnf  47097  liminflbuz2  47098  liminflimsupxrre  47100  cnrefiisplem  47112  xlimmnfvlem2  47116  xlimmnfv  47117  xlimpnfvlem2  47120  xlimpnfv  47121  xlimmnfmpt  47126  xlimpnfmpt  47127  climxlim2lem  47128  dfxlim2v  47130  xlimliminflimsup  47145  cncfuni  47169  icccncfext  47170  cncficcgt0  47171  cncfiooicclem1  47176  cncfiooiccre  47178  dvasinbx  47203  dvdsn1add  47222  dvnmul  47226  dvmptfprodlem  47227  dvnprodlem1  47229  dvnprodlem3  47231  iblspltprt  47256  itgioocnicc  47260  itgspltprt  47262  ismbl3  47269  stirlinglem5  47361  dirker2re  47375  dirkerper  47379  dirkertrigeq  47384  dirkercncflem2  47387  fourierdlem12  47402  fourierdlem15  47405  fourierdlem16  47406  fourierdlem20  47410  fourierdlem21  47411  fourierdlem22  47412  fourierdlem39  47429  fourierdlem40  47430  fourierdlem41  47431  fourierdlem42  47432  fourierdlem46  47435  fourierdlem49  47438  fourierdlem50  47439  fourierdlem57  47446  fourierdlem58  47447  fourierdlem59  47448  fourierdlem64  47453  fourierdlem65  47454  fourierdlem66  47455  fourierdlem68  47457  fourierdlem70  47459  fourierdlem71  47460  fourierdlem73  47462  fourierdlem78  47467  fourierdlem79  47468  fourierdlem80  47469  fourierdlem81  47470  fourierdlem82  47471  fourierdlem83  47472  fourierdlem87  47476  fourierdlem93  47482  fourierdlem95  47484  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem112  47501  sqwvfoura  47511  fourierswlem  47513  elaa2lem  47516  etransclem13  47530  etransclem23  47540  etransclem24  47541  etransclem32  47549  etransclem38  47555  etransclem46  47563  qndenserrnbllem  47577  rrxsnicc  47583  ioorrnopnlem  47587  prsal  47601  intsal  47613  salexct  47617  dfsalgen2  47624  issalnnd  47628  sge0rnre  47647  sge0val  47649  sge0z  47658  sge0revalmpt  47661  sge0tsms  47663  sge0pr  47677  sge0resplit  47689  sge0split  47692  sge0splitmpt  47694  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0fodjrnlem  47699  sge0iunmpt  47701  sge0rpcpnf  47704  sge0ltfirpmpt2  47709  sge0isum  47710  sge0xaddlem1  47716  sge0xaddlem2  47717  sge0pnffsumgt  47725  sge0gtfsumgt  47726  sge0seq  47729  sge0reuz  47730  nnfoctbdjlem  47738  nnfoctbdj  47739  meadjun  47745  meadjiunlem  47748  voliunsge0lem  47755  meaiuninc3v  47767  omeiunltfirp  47802  carageniuncllem2  47805  caratheodorylem1  47809  caratheodorylem2  47810  caratheodory  47811  isomenndlem  47813  isomennd  47814  hoicvr  47831  volicorescl  47836  ovnsubaddlem2  47854  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvle  47883  ovnhoilem2  47885  hspdifhsp  47899  hoiqssbllem2  47906  hoiqssbllem3  47907  hspmbllem2  47910  ovnsubadd2lem  47928  ovolval4lem1  47932  vonvolmbl  47944  vonioo  47965  vonicc  47968  pimrecltpos  47991  issmfle  48028  smflimlem1  48054  smflimlem2  48055  smflimlem6  48059  smfresal  48071  smfrec  48072  smfmullem4  48077  smfpimcc  48091  smflimmpt  48093  smfsuplem1  48094  smfsuplem3  48096  smfsupmpt  48098  smfsupxr  48099  smfinflem  48100  smfinfmpt  48102  smflimsuplem4  48106  smflimsuplem5  48107  smflimsupmpt  48112  smfliminfmpt  48115  fsupdm  48125  finfdm  48129  smonoord  48720  lswn0  48799  poprelb  48879  fmtnoprmfac1  48923  fmtnofac2lem  48926  sbgoldbst  49149  isgrim  49253  gpgedgvtx0  49432  snlindsntorlem  49913  1arymaptf  50084  ipolubdm  50432  ipoglbdm  50435  setc1onsubc  51071  aacllem  51367