Theorem adantll 713

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 579	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 206  df-an 396

This theorem is referenced by:  ad2antlr  726  ad2ant2l  745  ad2ant2lr  747  ad5ant23  759  ad5ant24  760  ad5ant25  761  3adant1  1128  3ad2antl3  1185  ralcom2  3370  vtocl2d  3547  sbc2iegf  3858  sbcralt  3865  pofun  5608  poinxp  5758  xpdifid  6172  sossfld  6190  preddowncl  6338  tz7.7  6395  onfr  6408  ssimaex  6983  eqfnun  7046  fndmdif  7051  dffo4  7113  fompt  7128  fcompt  7142  fconst2g  7215  f1cofveqaeq  7268  2f1fvneq  7270  isores3  7343  fvmptopabOLD  7475  limsssuc  7854  el2mpocl  8091  1stconst  8105  2ndconst  8106  curry1  8109  curry2  8112  poseq  8163  soseq  8164  extmptsuppeq  8193  suppss  8199  suppssOLD  8200  suppss2  8206  onnseq  8365  oe0  8543  oesuclem  8546  oecl  8558  oaordi  8567  oawordri  8571  omordi  8587  omword2  8595  omlimcl  8599  odi  8600  omass  8601  oeoe  8620  nnaordi  8639  oaabs  8669  omsmolem  8678  eceqoveq  8841  mapsnd  8905  dom2lem  9013  sbthlem9  9116  rexdif1en  9183  php3OLD  9249  onomeneqOLD  9254  isinf  9285  isinfOLD  9286  frfi  9313  fiint  9349  fodomfib  9351  fofinf1o  9352  marypha1lem  9457  ordiso2  9539  unwdomg  9608  xpwdomg  9609  frr1  9783  ac5num  10060  cff1  10282  cfcoflem  10296  infpssrlem4  10330  isf32lem9  10385  isf34lem7  10403  fin1a2lem13  10436  fin1a2s  10438  hsmexlem4  10453  axdc2lem  10472  zorn2lem6  10525  axpowndlem2  10622  inttsk  10798  tskuni  10807  nqereu  10953  prcdnq  11017  addclprlem2  11041  ltexpri  11067  prlem936  11071  reclem2pr  11072  axsup  11320  add4  11465  ltleadd  11728  lt2mul2div  12123  nn2ge  12270  zextle  12666  fnn0ind  12692  xrlttr  13152  ifle  13209  xnn0lem1lt  13256  xaddass  13261  xmulasslem3  13298  xlemul1a  13300  xadddilem  13306  xrsupsslem  13319  xrinfmsslem  13320  supxrunb1  13331  supxrunb2  13332  ixxin  13374  difreicc  13494  iccsplit  13495  iccshftr  13496  iccshftl  13498  iccdil  13500  icccntr  13502  fzaddel  13568  fzadd2  13569  fzrev  13597  modadd1  13906  modmul1  13922  fsuppmapnn0fiub  13989  mulexp  14099  expadd  14102  expmul  14105  expnbnd  14227  bccl  14314  hashdom  14371  prsshashgt1  14402  hashfacen  14446  hashfacenOLD  14447  brfi1uzind  14492  wrdnval  14528  swrdccat3blem  14722  revccat  14749  2shfti  15060  rexico  15333  cau3lem  15334  subcn2  15572  caucvgb  15659  iseraltlem1  15661  sumss  15703  fsumsplitsn  15723  incexclem  15815  supcvg  15835  mertenslem2  15864  fprodn0  15956  fprodsplitsn  15966  fprodle  15973  eftlcl  16084  reeftlcl  16085  rpnnen2lem6  16196  dvdsext  16298  3dvds  16308  sqoddm1div8z  16331  gcdcllem3  16476  bezoutr1  16540  seq1st  16542  dvdslcm  16569  lcmeq0  16571  lcmcl  16572  lcmneg  16574  lcmdvds  16579  coprmgcdb  16620  dvdsprime  16658  pc2dvds  16848  prmpwdvds  16873  unbenlem  16877  infpnlem1  16879  1arith  16896  vdwmc2  16948  ramcl  16998  mrcuni  17601  isacs1i  17637  acsfn  17639  funcpropd  17889  curfcl  18224  curf2ndf  18239  resmgmhm  18671  resmgmhm2b  18673  mgmhmco  18674  mgmhmima  18675  resmhm  18772  resmhm2b  18774  mhmco  18775  pwsdiagmhm  18783  gsumwsubmcl  18789  gsumwspan  18798  pwmnd  18889  dfgrp2  18919  subgint  19105  ghmmhmb  19181  resghm  19186  cntzmhm  19292  symgextf1lem  19375  f1omvdconj  19401  dfod2  19519  gexdvds  19539  subgpgp  19552  sylow1lem3  19555  frgpnabllem1  19828  dprdfeq0  19979  rhmimasubrnglem  20502  cntzsubrng  20504  cntzsubr  20545  isdrng2  20638  islmodd  20749  lsslss  20845  reslmhm2b  20939  rngqiprngimfo  21191  psgnfix1  21530  psgndif  21534  copsgndif  21535  ocvocv  21603  frlmsslsp  21730  frlmlbs  21731  psrbaglefi  21865  psrbaglefiOLD  21866  psrass23l  21910  psrass23  21912  psdmul  22090  mptcoe1fsupp  22134  psropprmul  22156  ply1coe  22217  mamudi  22316  mamudir  22317  mat1dimelbas  22386  scmatmulcl  22433  scmatfo  22445  mulmarep1gsum2  22489  mdetunilem7  22533  mdetunilem9  22535  gsummatr01lem3  22572  smadiadetlem3  22583  cpmadugsumlemF  22791  leordtval  23130  cnpnei  23181  cnco  23183  cnss1  23193  cmpsub  23317  hauscmplem  23323  dissnlocfin  23446  ptbasid  23492  tx2cn  23527  upxp  23540  txindis  23551  xkoptsub  23571  xkopt  23572  trfbas2  23760  filconn  23800  trfil2  23804  filssufilg  23828  ufileu  23836  fixufil  23839  ufilen  23847  rnelfmlem  23869  flimclsi  23895  hauspwpwf1  23904  fclsopn  23931  fclsfnflim  23944  fclscmpi  23946  alexsubALTlem4  23967  ptcmplem5  23973  tgpmulg  24010  subgtgp  24022  tgpt0  24036  tsmsxplem2  24071  metss  24430  metustfbas  24479  dscopn  24495  xrsmopn  24741  cncfss  24832  icoopnst  24876  iccpnfcnv  24882  icccvx  24888  evth  24898  phtpycc  24930  pcohtpylem  24959  lmmbrf  25203  fgcfil  25212  caucfil  25224  cfilres  25237  bcth3  25272  cmscsscms  25314  ovolfioo  25409  ovolficc  25410  voliunlem3  25494  volcn  25548  mbflimsup  25608  mbfi1fseqlem5  25662  itg2seq  25685  bddiblnc  25784  dvnff  25866  dvnadd  25872  cpnord  25878  c1liplem1  25942  plypf1  26159  plyaddlem1  26160  plymullem1  26161  coeeulem  26171  coeidlem  26184  dgrle  26190  dgrnznn  26194  plycjlem  26224  elqaalem3  26269  ulmcaulem  26343  ulmcau  26344  psergf  26361  psercn2  26372  psercn2OLD  26373  efopn  26605  abscxpbnd  26701  leibpi  26887  isppw2  27060  muinv  27138  bposlem3  27232  gausslemma2dlem4  27315  pntrmax  27510  pntpbnd1  27532  qabvexp  27572  madebday  27839  mulsrid  28026  peano5n0s  28204  eqeelen  28728  colinearalglem4  28733  axcgrid  28740  axsegconlem1  28741  axsegconlem3  28743  ax5seglem1  28752  ax5seglem2  28753  ax5seglem9  28761  axcontlem2  28789  cusgrfilem2  29283  vtxdgfisf  29303  usgr2pthlem  29590  uspgrn2crct  29632  crctcshwlkn0  29645  wwlksnext  29717  wwlksnextproplem3  29735  eupth2lem3lem4  30054  frgr3vlem1  30096  frgr3vlem2  30097  3vfriswmgrlem  30100  frgrwopreglem5  30144  numclwwlk3lem2  30207  grpoidinvlem3  30329  grpoidinv  30331  grpoideu  30332  nmoub3i  30596  nmlno0lem  30616  nmlnoubi  30619  ipasslem3  30656  ipblnfi  30678  hvaddsub4  30901  his35  30911  shsel3  31138  chj4  31358  spansncol  31391  chscllem2  31461  5oalem2  31478  3oalem2  31486  hoaddcl  31581  adjsym  31656  cnvadj  31715  hhcno  31727  hhcnf  31728  nmopub2tALT  31732  unoplin  31743  counop  31744  nmfnleub2  31749  hmoplin  31765  brafnmul  31774  nmlnop0iALT  31818  nmopun  31837  nmophmi  31854  riesz3i  31885  riesz1  31888  cnlnadjlem2  31891  cnlnadjlem6  31895  adjmul  31915  adjadd  31916  bra11  31931  cnvbraval  31933  kbass5  31943  kbass6  31944  leop2  31947  leopadd  31955  leopmuli  31956  leoptri  31959  leopnmid  31961  nmopleid  31962  pj3si  32030  hstel2  32042  cvcon3  32107  dmdmd  32123  dmdbr5  32131  mdsl0  32133  mdslmd1lem1  32148  mdslmd1lem2  32149  mdslmd3i  32155  superpos  32177  chirredlem2  32214  chirredlem3  32215  mdsymlem3  32228  mdsymlem5  32230  mdsymlem6  32231  sumdmdlem  32241  cdjreui  32255  cdj1i  32256  cdj3i  32264  foresf1o  32313  2ndimaxp  32446  abfmpel  32454  fcomptf  32457  fcnvgreu  32472  fdifsuppconst  32482  xrge0infss  32543  xnn0gt0  32552  cycpm2tr  32853  intlidl  33145  rhmpreimaprmidl  33180  lssdimle  33305  mdetpmtr1  33424  cmpcref  33451  xrge0iifcnv  33534  esumcst  33682  hasheuni  33704  esum2dlem  33711  esum2d  33712  sigaclcu2  33739  insiga  33756  unelldsys  33777  measres  33841  measdivcst  33843  volfiniune  33849  ddemeas  33855  sgn3da  34161  actfunsnf1o  34236  fnrelpredd  34712  fineqvac  34717  sconnpi1  34849  cvmsss2  34884  satfv1lem  34972  fmlaomn0  35000  gonarlem  35004  mrsubco  35131  dfon2lem6  35384  hfext  35779  elicc3  35801  fnessref  35841  bj-ismooredr2  36589  pibt2  36896  fin2solem  37079  fin2so  37080  lindsenlbs  37088  matunitlindflem1  37089  matunitlindflem2  37090  poimirlem2  37095  poimirlem14  37107  poimirlem25  37118  poimirlem26  37119  poimirlem29  37122  poimirlem30  37123  broucube  37127  heicant  37128  mblfinlem2  37131  mblfinlem3  37132  mblfinlem4  37133  ex-ovoliunnfl  37136  mbfresfi  37139  cnambfre  37141  itg2addnclem  37144  itg2addnclem2  37145  itg2addnc  37147  ftc1anclem3  37168  ftc1anclem4  37169  ftc1anclem5  37170  ftc1anclem6  37171  ftc1anclem7  37172  ftc1anclem8  37173  ftc1anc  37174  indexdom  37207  filbcmb  37213  fdc  37218  incsequz  37221  metf1o  37228  caures  37233  bndss  37259  ismtycnv  37275  heiborlem1  37284  rrncmslem  37305  isdrngo2  37431  rngoisocnv  37454  unichnidl  37504  erimeq2  38150  ax12eq  38413  ax12el  38414  lshpset2N  38591  pmapglb2N  39244  pmapglb2xN  39245  pclfinN  39373  polval2N  39379  cdleme31fv2  39866  cdleme32fvcl  39913  cdleme48gfv  40010  tendoicl  40269  tendoipl  40270  diaglbN  40528  dochkr1  40951  dochkr1OLDN  40952  evlsvvval  41796  selvcllem5  41815  evlselv  41820  fsuppind  41823  fsuppssind  41826  mhpind  41827  sumcubes  41873  dvdsexpim  41888  zaddcomlem  42006  zmulcomlem  42010  nacsfix  42132  eq0rabdioph  42196  diophren  42233  rencldnfilem  42240  pell1234qrdich  42281  jm2.24  42384  jm2.26lem3  42422  wepwsolem  42466  pwssplit4  42513  isnumbasgrplem3  42529  onexoegt  42672  onov0suclim  42703  cantnfresb  42753  omcl2  42762  ofoaid1  42787  ofoaid2  42788  grumnudlem  43722  cvgdvgrat  43750  ofsubid  43761  bcc0  43777  binomcxplemnn0  43786  uzwo4  44417  fiiuncl  44429  iunincfi  44460  nsstr  44461  rexanuz3  44462  iinssiin  44495  disjrnmpt2  44561  disjinfi  44565  choicefi  44573  fsneq  44579  difmap  44580  iunmapsn  44590  axccdom  44595  axccd  44602  rnmptlb  44619  rnmptbd2lem  44624  ssfiunibd  44691  supxrgelem  44719  suplesup  44721  xrlexaddrp  44734  xralrple2  44736  infxrunb2  44750  xralrple3  44756  xrralrecnnle  44765  xrralrecnnge  44772  supxrunb3  44781  unb2ltle  44797  rexabslelem  44800  supminfrnmpt  44827  infxrpnf  44828  supminfxr  44846  supminfxr2  44851  xrpnf  44868  pimxrneun  44871  cvgcaule  44874  iooiinicc  44927  ressioosup  44940  iooiinioc  44941  ressiooinf  44942  fsumsupp0  44966  divcnvg  45015  limcrecl  45017  sumnnodd  45018  islpcn  45027  lptre2pt  45028  limcresiooub  45030  limcresioolb  45031  limclner  45039  fnlimfvre  45062  allbutfifvre  45063  climinf3  45104  limsupmnflem  45108  limsupre3uzlem  45123  limsupreuzmpt  45127  climuzlem  45131  climisp  45134  climrescn  45136  climxrrelem  45137  climxrre  45138  climlimsupcex  45157  liminflelimsuplem  45163  limsupgtlem  45165  liminfvalxr  45171  liminfreuzlem  45190  liminfltlem  45192  liminflimsupclim  45195  xlimpnfxnegmnf  45202  liminflbuz2  45203  liminflimsupxrre  45205  cnrefiisplem  45217  xlimmnfvlem2  45221  xlimmnfv  45222  xlimpnfvlem2  45225  xlimpnfv  45226  xlimmnfmpt  45231  xlimpnfmpt  45232  climxlim2lem  45233  dfxlim2v  45235  xlimliminflimsup  45250  cncfuni  45274  icccncfext  45275  cncficcgt0  45276  cncfiooicclem1  45281  cncfiooiccre  45283  dvasinbx  45308  dvdsn1add  45327  dvnmul  45331  dvmptfprodlem  45332  dvnprodlem1  45334  dvnprodlem3  45336  iblspltprt  45361  itgioocnicc  45365  itgspltprt  45367  ismbl3  45374  stirlinglem5  45466  dirker2re  45480  dirkerper  45484  dirkertrigeq  45489  dirkercncflem2  45492  fourierdlem12  45507  fourierdlem15  45510  fourierdlem16  45511  fourierdlem20  45515  fourierdlem21  45516  fourierdlem22  45517  fourierdlem39  45534  fourierdlem40  45535  fourierdlem41  45536  fourierdlem42  45537  fourierdlem46  45540  fourierdlem49  45543  fourierdlem50  45544  fourierdlem57  45551  fourierdlem58  45552  fourierdlem59  45553  fourierdlem64  45558  fourierdlem65  45559  fourierdlem66  45560  fourierdlem68  45562  fourierdlem70  45564  fourierdlem71  45565  fourierdlem73  45567  fourierdlem78  45572  fourierdlem79  45573  fourierdlem80  45574  fourierdlem81  45575  fourierdlem82  45576  fourierdlem83  45577  fourierdlem87  45581  fourierdlem93  45587  fourierdlem95  45589  fourierdlem101  45595  fourierdlem103  45597  fourierdlem104  45598  fourierdlem111  45605  fourierdlem112  45606  sqwvfoura  45616  fourierswlem  45618  elaa2lem  45621  etransclem13  45635  etransclem23  45645  etransclem24  45646  etransclem32  45654  etransclem38  45660  etransclem46  45668  qndenserrnbllem  45682  rrxsnicc  45688  ioorrnopnlem  45692  prsal  45706  intsal  45718  salexct  45722  dfsalgen2  45729  issalnnd  45733  sge0rnre  45752  sge0val  45754  sge0z  45763  sge0revalmpt  45766  sge0tsms  45768  sge0pr  45782  sge0resplit  45794  sge0split  45797  sge0splitmpt  45799  sge0iunmptlemfi  45801  sge0iunmptlemre  45803  sge0fodjrnlem  45804  sge0iunmpt  45806  sge0rpcpnf  45809  sge0ltfirpmpt2  45814  sge0isum  45815  sge0xaddlem1  45821  sge0xaddlem2  45822  sge0pnffsumgt  45830  sge0gtfsumgt  45831  sge0seq  45834  sge0reuz  45835  nnfoctbdjlem  45843  nnfoctbdj  45844  meadjun  45850  meadjiunlem  45853  voliunsge0lem  45860  meaiuninc3v  45872  omeiunltfirp  45907  carageniuncllem2  45910  caratheodorylem1  45914  caratheodorylem2  45915  caratheodory  45916  isomenndlem  45918  isomennd  45919  hoicvr  45936  volicorescl  45941  ovnsubaddlem2  45959  hoidmvlelem2  45984  hoidmvlelem3  45985  hoidmvle  45988  ovnhoilem2  45990  hspdifhsp  46004  hoiqssbllem2  46011  hoiqssbllem3  46012  hspmbllem2  46015  ovnsubadd2lem  46033  ovolval4lem1  46037  vonvolmbl  46049  vonioo  46070  vonicc  46073  pimrecltpos  46096  issmfle  46133  smflimlem1  46159  smflimlem2  46160  smflimlem6  46164  smfresal  46176  smfrec  46177  smfmullem4  46182  smfpimcc  46196  smflimmpt  46198  smfsuplem1  46199  smfsuplem3  46201  smfsupmpt  46203  smfsupxr  46204  smfinflem  46205  smfinfmpt  46207  smflimsuplem4  46211  smflimsuplem5  46212  smflimsupmpt  46217  smfliminfmpt  46220  fsupdm  46230  finfdm  46234  smonoord  46711  lswn0  46784  poprelb  46864  fmtnoprmfac1  46905  fmtnofac2lem  46908  sbgoldbst  47118  isgrim  47166  snlindsntorlem  47538  1arymaptf  47714  ipolubdm  47998  ipoglbdm  48001  aacllem  48234