Theorem adantll 750

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ad2antlr  763  ad2ant2l  782  ad2ant2lr  784  3ad2antl3  1225  3adant1l  1318  ralcom2  3104  reu6  3395  sbc2iegf  3504  sbcralt  3510  pofun  5051  poinxp  5182  xpdifid  5562  sossfld  5580  predpo  5698  preddowncl  5707  tz7.7  5749  onfr  5763  ssimaex  6263  fndmdif  6321  dffo4  6375  foco2OLD  6380  fcompt  6400  fconst2g  6468  f1cofveqaeq  6515  2f1fvneq  6517  isores3  6585  fvmptopab  6697  limsssuc  7050  el2mpt2cl  7251  curry1  7269  curry2  7272  extmptsuppeq  7319  suppss  7325  suppssov1  7327  suppss2  7329  suppssfv  7331  onnseq  7441  oe0  7602  oesuclem  7605  oecl  7617  oaordi  7626  oawordri  7630  oaass  7641  omordi  7646  omword2  7654  omlimcl  7658  odi  7659  omass  7660  oeoe  7679  nnaordi  7698  oaabs  7724  omsmolem  7733  eceqoveq  7853  dom2lem  7995  sbthlem9  8078  php3  8146  onomeneq  8150  isinf  8173  frfi  8205  fiint  8237  fodomfib  8240  fofinf1o  8241  marypha1lem  8339  ordiso2  8420  unwdomg  8489  xpwdomg  8490  ac5num  8859  cff1  9080  cfcoflem  9094  infpssrlem4  9128  isf32lem9  9183  isf34lem7  9201  fin1a2lem13  9234  fin1a2s  9236  hsmexlem4  9251  axdc2lem  9270  zorn2lem6  9323  axpowndlem2  9420  inttsk  9596  tskuni  9605  nqereu  9751  prcdnq  9815  addclprlem2  9839  ltexpri  9865  prlem936  9869  reclem2pr  9870  axsup  10113  add4  10256  ltleadd  10511  lt2mul2div  10901  lediv12a  10916  nn2ge  11045  zextle  11450  fnn0ind  11476  xrlttr  11973  ifle  12028  xaddass  12079  xmulasslem3  12116  xlemul1a  12118  xadddilem  12124  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  ixxin  12192  difreicc  12304  iccsplit  12305  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  fzaddel  12375  fzadd2  12376  fzrev  12403  modadd1  12707  modmul1  12723  fsuppmapnn0fiub  12790  mulexp  12899  expadd  12902  expmul  12905  leexp1a  12919  expnbnd  12993  bccl  13109  hashdom  13168  prsshashgt1  13198  hashfacen  13238  brfi1uzind  13280  brfi1uzindOLD  13286  wrdnval  13335  swrdccat3blem  13495  revccat  13515  2shfti  13820  rexico  14093  cau3lem  14094  subcn2  14325  caucvgb  14410  iseraltlem1  14412  sumss  14455  fsumsplitsn  14474  incexclem  14568  supcvg  14588  mertenslem2  14617  fprodn0  14709  fprodsplitsn  14720  fprodle  14727  eftlcl  14837  reeftlcl  14838  rpnnen2lem6  14948  dvdsext  15043  3dvds  15052  3dvdsOLD  15053  sqoddm1div8z  15078  gcdcllem3  15223  bezoutr1  15282  seq1st  15284  dvdslcm  15311  lcmeq0  15313  lcmcl  15314  lcmneg  15316  lcmdvds  15321  coprmgcdb  15362  dvdsprime  15400  pc2dvds  15583  prmpwdvds  15608  unbenlem  15612  infpnlem1  15614  1arith  15631  vdwmc2  15683  ramcl  15733  mrcuni  16281  isacs1i  16318  acsfn  16320  funcpropd  16560  natpropd  16636  curfcl  16872  curf2ndf  16887  resmhm  17359  resmhm2b  17361  mhmco  17362  mhmima  17363  pwsdiagmhm  17369  gsumwsubmcl  17375  gsumwspan  17383  dfgrp2  17447  grpissubg  17614  subgint  17618  ghmmhmb  17671  resghm  17676  cntzmhm  17771  symgextf1lem  17840  f1omvdconj  17866  pmtr3ncom  17895  dfod2  17981  gexdvds  17999  subgpgp  18012  sylow1lem3  18015  frgpnabllem1  18276  dprdfeq0  18421  isdrng2  18757  cntzsubr  18812  islmodd  18869  lsslss  18961  reslmhm2b  19054  psrbaglefi  19372  mptcoe1fsupp  19585  ply1coe  19666  psgnfix1  19944  psgndif  19948  zrhcopsgndif  19949  ocvocv  20015  frlmsslsp  20135  frlmlbs  20136  mamudi  20209  mamudir  20210  mat1dimelbas  20277  scmatmulcl  20324  scmatfo  20336  mulmarep1gsum2  20380  mdetunilem7  20424  mdetunilem9  20426  gsummatr01lem3  20463  smadiadetlem3  20474  mp2pm2mplem4  20614  chfacfisf  20659  chfacfisfcpmat  20660  cpmadugsumlemF  20681  elcls  20877  leordtval  21017  cnpnei  21068  cnco  21070  cnss1  21080  cmpsub  21203  hauscmplem  21209  dissnlocfin  21332  ptbasid  21378  tx2cn  21413  upxp  21426  txindis  21437  xkoptsub  21457  xkopt  21458  trfbas2  21647  filconn  21687  trfil2  21691  filssufilg  21715  ufileu  21723  fixufil  21726  ufilen  21734  rnelfmlem  21756  flimclsi  21782  hauspwpwf1  21791  fclsopn  21818  fclsfnflim  21831  fclscmpi  21833  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem5  21860  tgpmulg  21897  subgtgp  21909  tgpt0  21922  tsmsxplem2  21957  metss  22313  metustfbas  22362  dscopn  22378  xrsmopn  22615  cncfss  22702  icoopnst  22738  iccpnfcnv  22743  icccvx  22749  evth  22758  phtpycc  22790  pcohtpylem  22819  lmmbrf  23060  fgcfil  23069  caucfil  23081  cfilres  23094  bcth3  23128  ovolfioo  23236  ovolficc  23237  voliunlem3  23320  volcn  23374  mbflimsup  23433  mbfi1fseqlem5  23486  itg2seq  23509  dvnff  23686  dvnadd  23692  cpnord  23698  c1liplem1  23759  plypf1  23968  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeidlem  23993  dgrle  23999  dgrnznn  24003  plycjlem  24032  elqaalem3  24076  ulmcaulem  24148  ulmcau  24149  psergf  24166  psercn2  24177  efopn  24404  abscxpbnd  24494  leibpi  24669  isppw2  24841  muinv  24919  bposlem3  25011  gausslemma2dlem4  25094  pntrmax  25253  pntpbnd1  25275  qabvexp  25315  eqeelen  25784  colinearalglem4  25789  axcgrid  25796  axsegconlem1  25797  axsegconlem3  25799  ax5seglem1  25808  ax5seglem2  25809  ax5seglem9  25817  axcontlem2  25845  cusgrfilem2  26352  vtxdgfisf  26372  usgr2pthlem  26659  uspgrn2crct  26700  crctcshwlkn0  26713  wwlksnextproplem3  26806  eupth2lem3lem4  27091  frgr3vlem1  27137  frgr3vlem2  27138  3vfriswmgrlem  27141  frgrwopreglem5  27185  extwwlkfablem1  27207  numclwwlk3lem  27241  grpoidinvlem3  27360  grpoidinv  27362  grpoideu  27363  nmoub3i  27628  nmlno0lem  27648  nmlnoubi  27651  ipasslem3  27688  ipblnfi  27711  hvaddsub4  27935  his35  27945  shsel3  28174  chj4  28394  spansncol  28427  chscllem2  28497  5oalem2  28514  3oalem2  28522  hoaddcl  28617  adjsym  28692  cnvadj  28751  hhcno  28763  hhcnf  28764  nmopub2tALT  28768  unoplin  28779  counop  28780  nmfnleub2  28785  hmoplin  28801  brafnmul  28810  nmlnop0iALT  28854  nmopun  28873  nmophmi  28890  riesz3i  28921  riesz1  28924  cnlnadjlem2  28927  cnlnadjlem6  28931  adjmul  28951  adjadd  28952  bra11  28967  cnvbraval  28969  kbass5  28979  kbass6  28980  leop2  28983  leopadd  28991  leopmuli  28992  leoptri  28995  leopnmid  28997  nmopleid  28998  pj3si  29066  hstel2  29078  cvcon3  29143  dmdmd  29159  dmdbr5  29167  mdsl0  29169  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd3i  29191  superpos  29213  chirredlem2  29250  chirredlem3  29251  mdsymlem3  29264  mdsymlem5  29266  mdsymlem6  29267  sumdmdlem  29277  cdjreui  29291  cdj1i  29292  cdj3i  29300  foresf1o  29343  abfmpel  29455  fcomptf  29458  fcnvgreu  29472  xrge0infss  29525  cmpcref  29917  xrge0iifcnv  29979  esumcst  30125  hasheuni  30147  esum2dlem  30154  esum2d  30155  sigaclcu2  30183  insiga  30200  unelldsys  30221  measres  30285  measdivcst  30288  volfiniune  30293  ddemeas  30299  sgn3da  30603  actfunsnf1o  30682  sconnpi1  31221  cvmsss2  31256  mrsubco  31418  dfon2lem6  31693  dftrpred3g  31733  poseq  31750  soseq  31751  hfext  32290  elicc3  32311  fnessref  32352  fin2solem  33395  fin2so  33396  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem2  33411  poimirlem14  33423  poimirlem25  33434  poimirlem26  33435  poimirlem29  33438  poimirlem30  33439  broucube  33443  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ex-ovoliunnfl  33452  mbfresfi  33456  cnambfre  33458  itg2addnclem  33461  itg2addnclem2  33462  itg2addnc  33464  bddiblnc  33480  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  eqfnun  33516  indexdom  33529  filbcmb  33535  fdc  33541  incsequz  33544  metf1o  33551  caures  33556  bndss  33585  ismtycnv  33601  heiborlem1  33610  rrncmslem  33631  isdrngo2  33757  rngoisocnv  33780  unichnidl  33830  ax12eq  34226  ax12el  34227  lshpset2N  34406  pmapglb2N  35057  pmapglb2xN  35058  pclfinN  35186  polval2N  35192  cdleme31fv2  35681  cdleme32fvcl  35728  cdleme48gfv  35825  tendoicl  36084  tendoipl  36085  diaglbN  36344  dochkr1  36767  dochkr1OLDN  36768  nacsfix  37275  eq0rabdioph  37340  diophren  37377  rencldnfilem  37384  pell1234qrdich  37425  jm2.24  37530  jm2.26lem3  37568  wepwsolem  37612  pwssplit4  37659  isnumbasgrplem3  37675  cvgdvgrat  38512  ofsubid  38523  bcc0  38539  binomcxplemnn0  38548  uzwo4  39221  fiiuncl  39234  iunincfi  39272  nsstr  39273  rexanuz3  39275  iinssiin  39312  ralimda  39326  disjrnmpt2  39375  fompt  39379  disjinfi  39380  mapsnd  39388  choicefi  39392  fsneq  39398  difmap  39399  iunmapsn  39409  axccdom  39416  axccd  39429  rnmptlb  39453  rnmptbd2lem  39463  ssfiunibd  39523  supxrgelem  39553  suplesup  39555  xrlexaddrp  39568  xralrple2  39570  infxrunb2  39584  xralrple3  39590  xrralrecnnle  39602  xrralrecnnge  39613  supxrunb3  39623  unb2ltle  39642  rexabslelem  39645  supminfrnmpt  39672  infxrpnf  39674  supminfxr  39694  supminfxr2  39699  iooiinicc  39769  ressioosup  39782  iooiinioc  39783  ressiooinf  39784  fsumsupp0  39810  divcnvg  39859  limcrecl  39861  sumnnodd  39862  islpcn  39871  lptre2pt  39872  limcresiooub  39874  limcresioolb  39875  limclner  39883  fnlimfvre  39906  allbutfifvre  39907  climinf3  39948  limsupmnflem  39952  limsupre3uzlem  39967  limsupreuzmpt  39971  climuzlem  39975  climisp  39978  climrescn  39980  climxrrelem  39981  climxrre  39982  climlimsupcex  40001  liminflelimsuplem  40007  limsupgtlem  40009  liminfvalxr  40015  liminfreuzlem  40034  liminfltlem  40036  liminflimsupclim  40039  cnrefiisplem  40055  xlimmnfvlem2  40059  xlimmnfv  40060  xlimpnfvlem2  40063  xlimpnfv  40064  xlimmnfmpt  40069  xlimpnfmpt  40070  climxlim2lem  40071  dfxlim2v  40073  cncfuni  40099  icccncfext  40100  cncficcgt0  40101  cncfiooicclem1  40106  cncfiooiccre  40108  dvasinbx  40135  dvdsn1add  40154  dvnmul  40158  dvmptfprodlem  40159  dvnprodlem1  40161  dvnprodlem3  40163  iblspltprt  40189  itgioocnicc  40193  itgspltprt  40195  ismbl3  40203  stirlinglem5  40295  dirker2re  40309  dirkerper  40313  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem12  40336  fourierdlem15  40339  fourierdlem16  40340  fourierdlem20  40344  fourierdlem21  40345  fourierdlem22  40346  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem46  40369  fourierdlem49  40372  fourierdlem50  40373  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem64  40387  fourierdlem65  40388  fourierdlem66  40389  fourierdlem68  40391  fourierdlem70  40393  fourierdlem71  40394  fourierdlem73  40396  fourierdlem78  40401  fourierdlem79  40402  fourierdlem80  40403  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem87  40410  fourierdlem93  40416  fourierdlem95  40418  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  sqwvfoura  40445  fourierswlem  40447  elaa2lem  40450  etransclem13  40464  etransclem23  40474  etransclem24  40475  etransclem32  40483  etransclem38  40489  etransclem46  40497  qndenserrnbllem  40514  rrxsnicc  40520  ioorrnopnlem  40524  prsal  40538  intsal  40548  salexct  40552  dfsalgen2  40559  issalnnd  40563  sge0rnre  40581  sge0val  40583  sge0z  40592  sge0revalmpt  40595  sge0tsms  40597  sge0pr  40611  sge0resplit  40623  sge0split  40626  sge0splitmpt  40628  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0fodjrnlem  40633  sge0iunmpt  40635  sge0rpcpnf  40638  sge0ltfirpmpt2  40643  sge0isum  40644  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0pnffsumgt  40659  sge0gtfsumgt  40660  sge0seq  40663  sge0reuz  40664  nnfoctbdjlem  40672  nnfoctbdj  40673  meadjun  40679  meadjiunlem  40682  voliunsge0lem  40689  omeiunltfirp  40733  carageniuncllem2  40736  caratheodorylem1  40740  caratheodorylem2  40741  caratheodory  40742  isomenndlem  40744  isomennd  40745  hoicvr  40762  volicorescl  40767  ovnsubaddlem2  40785  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvle  40814  ovnhoilem2  40816  hspdifhsp  40830  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem2  40841  ovnsubadd2lem  40859  ovolval4lem1  40863  vonvolmbl  40875  vonioo  40896  vonicc  40899  pimrecltpos  40919  issmfle  40954  smflimlem1  40979  smflimlem2  40980  smflimlem6  40984  smfresal  40995  smfrec  40996  smfmullem4  41001  smfpimcc  41014  smflimmpt  41016  smfsuplem1  41017  smfsuplem3  41019  smfsupmpt  41021  smfsupxr  41022  smfinflem  41023  smfinfmpt  41025  smflimsuplem4  41029  smflimsuplem5  41030  smflimsupmpt  41035  smfliminfmpt  41038  smonoord  41341  lswn0  41380  fmtnoprmfac1  41477  fmtnofac2lem  41480  sbgoldbst  41666  resmgmhm  41798  resmgmhm2b  41800  mgmhmco  41801  mgmhmima  41802  snlindsntorlem  42259  aacllem  42547