Theorem adantll 724

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 589	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 209  df-an 400

This theorem is referenced by:  ad2antlr  737  ad2ant2l  756  ad2ant2lr  758  ad5ant23  769  ad5ant24  770  ad5ant25  771  3adant1  1142  3ad2antl3  1200  ralcom2  3363  vtocl2d  3527  sbc2iegf  3816  sbcralt  3823  pofun  5569  poinxp  5724  xpdifid  6149  sossfld  6167  preddowncl  6314  tz7.7  6367  onfr  6380  ssimaex  6947  fsneq  7011  eqfnun  7013  fndmdif  7018  dffo4  7079  fompt  7094  fcompt  7110  fconst2g  7182  f1cofveqaeq  7236  isores3  7314  limsssuc  7825  el2mpocl  8059  1stconst  8073  2ndconst  8074  curry1  8077  curry2  8080  poseq  8132  soseq  8133  extmptsuppeq  8162  suppss  8168  suppss2  8174  onnseq  8309  oe0  8485  oesuclem  8488  oecl  8500  oaordi  8509  oawordri  8513  omordi  8529  omword2  8537  omlimcl  8541  odi  8542  omass  8543  oeoe  8563  nnaordi  8582  oaabs  8612  omsmolem  8621  eceqoveq  8798  mapsnd  8862  dom2lem  8967  sbthlem9  9061  rexdif1en  9123  isinf  9203  frfi  9223  fiint  9265  fodomfib  9267  fodomfibOLD  9268  fofinf1o  9269  marypha1lem  9373  ordiso2  9457  unwdomg  9526  xpwdomg  9527  frr1  9711  ac5num  9986  cff1  10209  cfcoflem  10223  infpssrlem4  10257  isf32lem9  10312  isf34lem7  10330  fin1a2lem13  10363  fin1a2s  10365  hsmexlem4  10380  axdc2lem  10399  zorn2lem6  10452  axpowndlem2  10550  inttsk  10726  tskuni  10735  nqereu  10881  prcdnq  10945  addclprlem2  10969  ltexpri  10995  prlem936  10999  reclem2pr  11000  axsup  11252  add4  11398  ltleadd  11664  lt2mul2div  12064  nn2ge  12234  zextle  12640  fnn0ind  12666  xrlttr  13136  ifle  13194  xnn0lem1lt  13241  xaddass  13246  xmulasslem3  13283  xlemul1a  13285  xadddilem  13291  xrsupsslem  13304  xrinfmsslem  13305  supxrunb1  13316  supxrunb2  13317  ixxin  13360  difreicc  13482  iccsplit  13483  iccshftr  13484  iccshftl  13486  iccdil  13488  icccntr  13490  fzaddel  13557  fzadd2  13558  fzrev  13586  modadd1  13912  modmul1  13931  fsuppmapnn0fiub  13998  mulexp  14108  expadd  14111  expmul  14114  expnbnd  14239  bccl  14329  hashdom  14386  prsshashgt1  14417  hashfacen  14461  brfi1uzind  14515  wrdnval  14552  swrdccat3blem  14746  revccat  14773  2shfti  15087  sgn3da  15105  rexico  15372  cau3lem  15373  subcn2  15613  caucvgb  15698  iseraltlem1  15700  sumss  15742  fsumsplitsn  15762  incexclem  15857  supcvg  15877  mertenslem2  15906  fprodn0  16000  fprodsplitsn  16010  fprodle  16017  eftlcl  16130  reeftlcl  16131  rpnnen2lem6  16242  dvdsext  16346  3dvds  16356  sqoddm1div8z  16379  gcdcllem3  16526  dvdsexpim  16580  bezoutr1  16594  seq1st  16596  dvdslcm  16623  lcmeq0  16625  lcmcl  16626  lcmneg  16628  lcmdvds  16633  coprmgcdb  16674  dvdsprime  16712  pc2dvds  16906  prmpwdvds  16931  unbenlem  16935  infpnlem1  16937  1arith  16954  vdwmc2  17006  ramcl  17056  mrcuni  17644  isacs1i  17680  acsfn  17682  funcpropd  17926  curfcl  18255  curf2ndf  18270  resmgmhm  18736  resmgmhm2b  18738  mgmhmco  18739  mgmhmima  18740  resmhm  18845  resmhm2b  18847  mhmco  18848  pwsdiagmhm  18856  gsumwsubmcl  18862  gsumwspan  18871  pwmnd  18965  dfgrp2  18995  subgint  19183  ghmmhmb  19258  resghm  19263  cntzmhm  19372  symgextf1lem  19451  f1omvdconj  19477  dfod2  19595  gexdvds  19615  subgpgp  19628  sylow1lem3  19631  frgpnabllem1  19904  dprdfeq0  20055  rhmimasubrnglem  20602  cntzsubrng  20604  cntzsubr  20643  isdrng2  20780  islmodd  20921  lsslss  21016  reslmhm2b  21109  rngqiprngimfo  21359  psgnfix1  21638  psgndif  21642  copsgndif  21643  ocvocv  21711  frlmsslsp  21836  frlmlbs  21837  psrbaglefi  21966  psrdi  22004  psrass23l  22006  psrass23  22008  evlsvvval  22134  rhmcomulmpl  22165  selvcllem5  22180  psdmul  22219  mptcoe1fsupp  22265  psropprmul  22287  ply1coe  22349  mamudi  22451  mamudir  22452  mat1dimelbas  22519  scmatmulcl  22566  scmatfo  22578  mulmarep1gsum2  22622  mdetunilem7  22666  mdetunilem9  22668  gsummatr01lem3  22705  smadiadetlem3  22716  cpmadugsumlemF  22924  leordtval  23261  cnpnei  23312  cnco  23314  cnss1  23324  cmpsub  23448  hauscmplem  23454  dissnlocfin  23577  ptbasid  23623  tx2cn  23658  upxp  23671  txindis  23682  xkoptsub  23702  xkopt  23703  trfbas2  23891  filconn  23931  trfil2  23935  filssufilg  23959  ufileu  23967  fixufil  23970  ufilen  23978  rnelfmlem  24000  flimclsi  24026  hauspwpwf1  24035  fclsopn  24062  fclsfnflim  24075  fclscmpi  24077  alexsubALTlem4  24098  ptcmplem5  24104  tgpmulg  24141  subgtgp  24153  tgpt0  24167  tsmsxplem2  24202  metss  24556  metustfbas  24605  dscopn  24621  xrsmopn  24861  cncfss  24949  icoopnst  24989  iccpnfcnv  24994  icccvx  25000  evth  25009  phtpycc  25041  pcohtpylem  25069  lmmbrf  25312  fgcfil  25321  caucfil  25333  cfilres  25346  bcth3  25381  cmscsscms  25423  ovolfioo  25517  ovolficc  25518  voliunlem3  25602  volcn  25656  mbflimsup  25716  mbfi1fseqlem5  25769  itg2seq  25792  bddiblnc  25892  dvnff  25973  dvnadd  25979  cpnord  25985  c1liplem1  26046  plypf1  26260  plyaddlem1  26261  plymullem1  26262  coeeulem  26272  coeidlem  26285  dgrle  26291  dgrnznn  26295  plycjlem  26324  elqaalem3  26373  ulmcaulem  26445  ulmcau  26446  psergf  26463  psercn2  26474  efopn  26711  abscxpbnd  26806  leibpi  26995  isppw2  27167  muinv  27245  bposlem3  27338  gausslemma2dlem4  27421  pntrmax  27616  pntpbnd1  27638  qabvexp  27678  madebday  27981  mulsrid  28194  bdayons  28357  peano5n0s  28400  bdaypw2n0bndlem  28544  bdayfinlem  28567  eqeelen  29062  colinearalglem4  29067  axcgrid  29074  axsegconlem1  29075  axsegconlem3  29077  ax5seglem1  29086  ax5seglem2  29087  ax5seglem9  29095  axcontlem2  29123  cusgrfilem2  29614  vtxdgfisf  29634  usgr2pthlem  29920  uspgrn2crct  29965  crctcshwlkn0  29978  wwlksnext  30050  wwlksnextproplem3  30068  eupth2lem3lem4  30390  frgr3vlem1  30432  frgr3vlem2  30433  3vfriswmgrlem  30436  frgrwopreglem5  30480  numclwwlk3lem2  30543  grpoidinvlem3  30666  grpoidinv  30668  grpoideu  30669  nmoub3i  30933  nmlno0lem  30953  nmlnoubi  30956  ipasslem3  30993  ipblnfi  31015  hvaddsub4  31238  his35  31248  shsel3  31475  chj4  31695  spansncol  31728  chscllem2  31798  5oalem2  31815  3oalem2  31823  hoaddcl  31918  adjsym  31993  cnvadj  32052  hhcno  32064  hhcnf  32065  nmopub2tALT  32069  unoplin  32080  counop  32081  nmfnleub2  32086  hmoplin  32102  brafnmul  32111  nmlnop0iALT  32155  nmopun  32174  nmophmi  32191  riesz3i  32222  riesz1  32225  cnlnadjlem2  32228  cnlnadjlem6  32232  adjmul  32252  adjadd  32253  bra11  32268  cnvbraval  32270  kbass5  32280  kbass6  32281  leop2  32284  leopadd  32292  leopmuli  32293  leoptri  32296  leopnmid  32298  nmopleid  32299  pj3si  32367  hstel2  32379  cvcon3  32444  dmdmd  32460  dmdbr5  32468  mdsl0  32470  mdslmd1lem1  32485  mdslmd1lem2  32486  mdslmd3i  32492  superpos  32514  chirredlem2  32551  chirredlem3  32552  mdsymlem3  32565  mdsymlem5  32567  mdsymlem6  32568  sumdmdlem  32578  cdjreui  32592  cdj1i  32593  cdj3i  32601  foresf1o  32663  2ndimaxp  32809  abfmpel  32818  fcomptf  32821  fcnvgreu  32835  fdifsuppconst  32852  xrge0infss  32923  xnn0gt0  32932  cycpm2tr  33260  elrgspnlem2  33385  elrgspnlem3  33386  intlidl  33567  rhmpreimaprmidl  33599  mplvrpmga  33803  psrmonmul  33808  esplyfval0  33822  vieta  33838  lssdimle  33866  mdetpmtr1  34081  cmpcref  34108  xrge0iifcnv  34191  zrhcntr  34237  esumcst  34321  hasheuni  34343  esum2dlem  34350  esum2d  34351  sigaclcu2  34378  insiga  34395  unelldsys  34416  measres  34480  measdivcst  34482  volfiniune  34488  ddemeas  34494  actfunsnf1o  34859  fnrelpredd  35348  fineqvac  35373  fineqvnttrclselem1  35378  sconnpi1  35550  cvmsss2  35585  satfv1lem  35673  fmlaomn0  35701  gonarlem  35705  mrsubco  35832  dfon2lem6  36097  hfext  36494  elicc3  36638  fnessref  36678  bj-ismooredr2  37561  pibt2  37872  fin2solem  38066  fin2so  38067  lindsenlbs  38075  matunitlindflem1  38076  matunitlindflem2  38077  poimirlem2  38082  poimirlem14  38094  poimirlem25  38105  poimirlem26  38106  poimirlem29  38109  poimirlem30  38110  broucube  38114  heicant  38115  mblfinlem2  38118  mblfinlem3  38119  mblfinlem4  38120  ex-ovoliunnfl  38123  mbfresfi  38126  cnambfre  38128  itg2addnclem  38131  itg2addnclem2  38132  itg2addnc  38134  ftc1anclem3  38155  ftc1anclem4  38156  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  indexdom  38194  filbcmb  38200  fdc  38205  incsequz  38208  metf1o  38215  caures  38220  bndss  38246  ismtycnv  38262  heiborlem1  38271  rrncmslem  38292  isdrngo2  38418  rngoisocnv  38441  unichnidl  38491  erimeq2  39223  ax12eq  39526  ax12el  39527  lshpset2N  39704  pmapglb2N  40356  pmapglb2xN  40357  pclfinN  40485  polval2N  40491  cdleme31fv2  40978  cdleme32fvcl  41025  cdleme48gfv  41122  tendoicl  41381  tendoipl  41382  diaglbN  41640  dochkr1  42063  dochkr1OLDN  42064  sumcubes  42883  expeq1d  42894  zaddcomlem  43046  zmulcomlem  43050  fiabv  43115  rhmcomulpsr  43125  evlselv  43132  fsuppind  43133  fsuppssind  43136  mhpind  43137  nacsfix  43254  eq0rabdioph  43318  diophren  43351  rencldnfilem  43358  pell1234qrdich  43399  jm2.24  43501  jm2.26lem3  43539  wepwsolem  43580  pwssplit4  43627  isnumbasgrplem3  43643  onexoegt  43782  onov0suclim  43812  cantnfresb  43862  omcl2  43871  ofoaid1  43896  ofoaid2  43897  grumnudlem  44822  cvgdvgrat  44850  ofsubid  44861  bcc0  44877  binomcxplemnn0  44886  uzwo4  45594  fiiuncl  45606  iunincfi  45633  nsstr  45634  rexanuz3  45635  iinssiin  45668  disjrnmpt2  45727  disjinfi  45731  choicefi  45738  difmap  45744  iunmapsn  45754  axccdom  45759  axccd  45765  rnmptlb  45779  rnmptbd2lem  45784  ssfiunibd  45849  supxrgelem  45874  suplesup  45876  xrlexaddrp  45889  xralrple2  45891  infxrunb2  45904  xralrple3  45910  xrralrecnnle  45919  xrralrecnnge  45926  supxrunb3  45935  unb2ltle  45950  rexabslelem  45953  supminfrnmpt  45980  infxrpnf  45981  supminfxr  45999  supminfxr2  46004  xrpnf  46020  pimxrneun  46023  cvgcaule  46026  iooiinicc  46079  ressioosup  46092  iooiinioc  46093  ressiooinf  46094  fsumsupp0  46115  divcnvg  46164  limcrecl  46166  sumnnodd  46167  islpcn  46174  lptre2pt  46175  limcresiooub  46177  limcresioolb  46178  limclner  46186  fnlimfvre  46209  allbutfifvre  46210  climinf3  46251  limsupmnflem  46255  limsupre3uzlem  46270  limsupreuzmpt  46274  climuzlem  46278  climisp  46281  climrescn  46283  climxrrelem  46284  climxrre  46285  climlimsupcex  46304  liminflelimsuplem  46310  limsupgtlem  46312  liminfvalxr  46318  liminfreuzlem  46337  liminfltlem  46339  liminflimsupclim  46342  xlimpnfxnegmnf  46349  liminflbuz2  46350  liminflimsupxrre  46352  cnrefiisplem  46364  xlimmnfvlem2  46368  xlimmnfv  46369  xlimpnfvlem2  46372  xlimpnfv  46373  xlimmnfmpt  46378  xlimpnfmpt  46379  climxlim2lem  46380  dfxlim2v  46382  xlimliminflimsup  46397  cncfuni  46421  icccncfext  46422  cncficcgt0  46423  cncfiooicclem1  46428  cncfiooiccre  46430  dvasinbx  46455  dvdsn1add  46474  dvnmul  46478  dvmptfprodlem  46479  dvnprodlem1  46481  dvnprodlem3  46483  iblspltprt  46508  itgioocnicc  46512  itgspltprt  46514  ismbl3  46521  stirlinglem5  46613  dirker2re  46627  dirkerper  46631  dirkertrigeq  46636  dirkercncflem2  46639  fourierdlem12  46654  fourierdlem15  46657  fourierdlem16  46658  fourierdlem20  46662  fourierdlem21  46663  fourierdlem22  46664  fourierdlem39  46681  fourierdlem40  46682  fourierdlem41  46683  fourierdlem42  46684  fourierdlem46  46687  fourierdlem49  46690  fourierdlem50  46691  fourierdlem57  46698  fourierdlem58  46699  fourierdlem59  46700  fourierdlem64  46705  fourierdlem65  46706  fourierdlem66  46707  fourierdlem68  46709  fourierdlem70  46711  fourierdlem71  46712  fourierdlem73  46714  fourierdlem78  46719  fourierdlem79  46720  fourierdlem80  46721  fourierdlem81  46722  fourierdlem82  46723  fourierdlem83  46724  fourierdlem87  46728  fourierdlem93  46734  fourierdlem95  46736  fourierdlem101  46742  fourierdlem103  46744  fourierdlem104  46745  fourierdlem111  46752  fourierdlem112  46753  sqwvfoura  46763  fourierswlem  46765  elaa2lem  46768  etransclem13  46782  etransclem23  46792  etransclem24  46793  etransclem32  46801  etransclem38  46807  etransclem46  46815  qndenserrnbllem  46829  rrxsnicc  46835  ioorrnopnlem  46839  prsal  46853  intsal  46865  salexct  46869  dfsalgen2  46876  issalnnd  46880  sge0rnre  46899  sge0val  46901  sge0z  46910  sge0revalmpt  46913  sge0tsms  46915  sge0pr  46929  sge0resplit  46941  sge0split  46944  sge0splitmpt  46946  sge0iunmptlemfi  46948  sge0iunmptlemre  46950  sge0fodjrnlem  46951  sge0iunmpt  46953  sge0rpcpnf  46956  sge0ltfirpmpt2  46961  sge0isum  46962  sge0xaddlem1  46968  sge0xaddlem2  46969  sge0pnffsumgt  46977  sge0gtfsumgt  46978  sge0seq  46981  sge0reuz  46982  nnfoctbdjlem  46990  nnfoctbdj  46991  meadjun  46997  meadjiunlem  47000  voliunsge0lem  47007  meaiuninc3v  47019  omeiunltfirp  47054  carageniuncllem2  47057  caratheodorylem1  47061  caratheodorylem2  47062  caratheodory  47063  isomenndlem  47065  isomennd  47066  hoicvr  47083  volicorescl  47088  ovnsubaddlem2  47106  hoidmvlelem2  47131  hoidmvlelem3  47132  hoidmvle  47135  ovnhoilem2  47137  hspdifhsp  47151  hoiqssbllem2  47158  hoiqssbllem3  47159  hspmbllem2  47162  ovnsubadd2lem  47180  ovolval4lem1  47184  vonvolmbl  47196  vonioo  47217  vonicc  47220  pimrecltpos  47243  issmfle  47280  smflimlem1  47306  smflimlem2  47307  smflimlem6  47311  smfresal  47323  smfrec  47324  smfmullem4  47329  smfpimcc  47343  smflimmpt  47345  smfsuplem1  47346  smfsuplem3  47348  smfsupmpt  47350  smfsupxr  47351  smfinflem  47352  smfinfmpt  47354  smflimsuplem4  47358  smflimsuplem5  47359  smflimsupmpt  47364  smfliminfmpt  47367  fsupdm  47377  finfdm  47381  smonoord  47932  lswn0  48011  poprelb  48091  fmtnoprmfac1  48135  fmtnofac2lem  48138  sbgoldbst  48361  isgrim  48465  gpgedgvtx0  48644  snlindsntorlem  49053  1arymaptf  49224  ipolubdm  49569  ipoglbdm  49572  setc1onsubc  50184  aacllem  50383