Theorem adantll 712

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  ad2antlr  725  ad2ant2l  744  ad2ant2lr  746  ad5ant23  758  ad5ant24  759  ad5ant25  760  3adant1  1130  3ad2antl3  1187  ralcom2  3373  vtocl2d  3544  sbc2iegf  3859  sbcralt  3866  pofun  5606  poinxp  5756  xpdifid  6167  sossfld  6185  preddowncl  6333  tz7.7  6390  onfr  6403  ssimaex  6976  eqfnun  7038  fndmdif  7043  dffo4  7104  fompt  7119  fcompt  7133  fconst2g  7206  f1cofveqaeq  7259  2f1fvneq  7261  isores3  7334  fvmptopabOLD  7466  limsssuc  7841  el2mpocl  8074  1stconst  8088  2ndconst  8089  curry1  8092  curry2  8095  poseq  8146  soseq  8147  extmptsuppeq  8175  suppss  8181  suppssOLD  8182  suppssov1  8185  suppss2  8187  onnseq  8346  oe0  8524  oesuclem  8527  oecl  8539  oaordi  8548  oawordri  8552  omordi  8568  omword2  8576  omlimcl  8580  odi  8581  omass  8582  oeoe  8601  nnaordi  8620  oaabs  8649  omsmolem  8658  eceqoveq  8818  mapsnd  8882  dom2lem  8990  sbthlem9  9093  rexdif1en  9160  php3OLD  9226  onomeneqOLD  9231  isinf  9262  isinfOLD  9263  frfi  9290  fiint  9326  fodomfib  9328  fofinf1o  9329  marypha1lem  9430  ordiso2  9512  unwdomg  9581  xpwdomg  9582  frr1  9756  ac5num  10033  cff1  10255  cfcoflem  10269  infpssrlem4  10303  isf32lem9  10358  isf34lem7  10376  fin1a2lem13  10409  fin1a2s  10411  hsmexlem4  10426  axdc2lem  10445  zorn2lem6  10498  axpowndlem2  10595  inttsk  10771  tskuni  10780  nqereu  10926  prcdnq  10990  addclprlem2  11014  ltexpri  11040  prlem936  11044  reclem2pr  11045  axsup  11293  add4  11438  ltleadd  11701  lt2mul2div  12096  nn2ge  12243  zextle  12639  fnn0ind  12665  xrlttr  13123  ifle  13180  xnn0lem1lt  13227  xaddass  13232  xmulasslem3  13269  xlemul1a  13271  xadddilem  13277  xrsupsslem  13290  xrinfmsslem  13291  supxrunb1  13302  supxrunb2  13303  ixxin  13345  difreicc  13465  iccsplit  13466  iccshftr  13467  iccshftl  13469  iccdil  13471  icccntr  13473  fzaddel  13539  fzadd2  13540  fzrev  13568  modadd1  13877  modmul1  13893  fsuppmapnn0fiub  13960  mulexp  14071  expadd  14074  expmul  14077  expnbnd  14199  bccl  14286  hashdom  14343  prsshashgt1  14374  hashfacen  14417  hashfacenOLD  14418  brfi1uzind  14463  wrdnval  14499  swrdccat3blem  14693  revccat  14720  2shfti  15031  rexico  15304  cau3lem  15305  subcn2  15543  caucvgb  15630  iseraltlem1  15632  sumss  15674  fsumsplitsn  15694  incexclem  15786  supcvg  15806  mertenslem2  15835  fprodn0  15927  fprodsplitsn  15937  fprodle  15944  eftlcl  16054  reeftlcl  16055  rpnnen2lem6  16166  dvdsext  16268  3dvds  16278  sqoddm1div8z  16301  gcdcllem3  16446  bezoutr1  16510  seq1st  16512  dvdslcm  16539  lcmeq0  16541  lcmcl  16542  lcmneg  16544  lcmdvds  16549  coprmgcdb  16590  dvdsprime  16628  pc2dvds  16816  prmpwdvds  16841  unbenlem  16845  infpnlem1  16847  1arith  16864  vdwmc2  16916  ramcl  16966  mrcuni  17569  isacs1i  17605  acsfn  17607  funcpropd  17855  curfcl  18189  curf2ndf  18204  resmgmhm  18636  resmgmhm2b  18638  mgmhmco  18639  mgmhmima  18640  resmhm  18737  resmhm2b  18739  mhmco  18740  pwsdiagmhm  18748  gsumwsubmcl  18754  gsumwspan  18763  pwmnd  18854  dfgrp2  18883  subgint  19066  ghmmhmb  19141  resghm  19146  cntzmhm  19246  symgextf1lem  19329  f1omvdconj  19355  dfod2  19473  gexdvds  19493  subgpgp  19506  sylow1lem3  19509  frgpnabllem1  19782  dprdfeq0  19933  rhmimasubrnglem  20453  cntzsubrng  20455  cntzsubr  20496  isdrng2  20514  islmodd  20620  lsslss  20716  reslmhm2b  20809  rngqiprngimfo  21060  psgnfix1  21370  psgndif  21374  copsgndif  21375  ocvocv  21443  frlmsslsp  21570  frlmlbs  21571  psrbaglefi  21704  psrbaglefiOLD  21705  psrass23l  21747  psrass23  21749  mptcoe1fsupp  21958  psropprmul  21980  ply1coe  22040  mamudi  22123  mamudir  22124  mat1dimelbas  22193  scmatmulcl  22240  scmatfo  22252  mulmarep1gsum2  22296  mdetunilem7  22340  mdetunilem9  22342  gsummatr01lem3  22379  smadiadetlem3  22390  cpmadugsumlemF  22598  leordtval  22937  cnpnei  22988  cnco  22990  cnss1  23000  cmpsub  23124  hauscmplem  23130  dissnlocfin  23253  ptbasid  23299  tx2cn  23334  upxp  23347  txindis  23358  xkoptsub  23378  xkopt  23379  trfbas2  23567  filconn  23607  trfil2  23611  filssufilg  23635  ufileu  23643  fixufil  23646  ufilen  23654  rnelfmlem  23676  flimclsi  23702  hauspwpwf1  23711  fclsopn  23738  fclsfnflim  23751  fclscmpi  23753  alexsubALTlem4  23774  ptcmplem5  23780  tgpmulg  23817  subgtgp  23829  tgpt0  23843  tsmsxplem2  23878  metss  24237  metustfbas  24286  dscopn  24302  xrsmopn  24548  cncfss  24639  icoopnst  24679  iccpnfcnv  24684  icccvx  24690  evth  24699  phtpycc  24731  pcohtpylem  24759  lmmbrf  25003  fgcfil  25012  caucfil  25024  cfilres  25037  bcth3  25072  cmscsscms  25114  ovolfioo  25208  ovolficc  25209  voliunlem3  25293  volcn  25347  mbflimsup  25407  mbfi1fseqlem5  25461  itg2seq  25484  bddiblnc  25583  dvnff  25664  dvnadd  25670  cpnord  25676  c1liplem1  25737  plypf1  25950  plyaddlem1  25951  plymullem1  25952  coeeulem  25962  coeidlem  25975  dgrle  25981  dgrnznn  25985  plycjlem  26014  elqaalem3  26058  ulmcaulem  26130  ulmcau  26131  psergf  26148  psercn2  26159  efopn  26390  abscxpbnd  26485  leibpi  26671  isppw2  26843  muinv  26921  bposlem3  27013  gausslemma2dlem4  27096  pntrmax  27291  pntpbnd1  27313  qabvexp  27353  madebday  27619  mulsrid  27796  eqeelen  28417  colinearalglem4  28422  axcgrid  28429  axsegconlem1  28430  axsegconlem3  28432  ax5seglem1  28441  ax5seglem2  28442  ax5seglem9  28450  axcontlem2  28478  cusgrfilem2  28968  vtxdgfisf  28988  usgr2pthlem  29275  uspgrn2crct  29317  crctcshwlkn0  29330  wwlksnext  29402  wwlksnextproplem3  29420  eupth2lem3lem4  29739  frgr3vlem1  29781  frgr3vlem2  29782  3vfriswmgrlem  29785  frgrwopreglem5  29829  numclwwlk3lem2  29892  grpoidinvlem3  30014  grpoidinv  30016  grpoideu  30017  nmoub3i  30281  nmlno0lem  30301  nmlnoubi  30304  ipasslem3  30341  ipblnfi  30363  hvaddsub4  30586  his35  30596  shsel3  30823  chj4  31043  spansncol  31076  chscllem2  31146  5oalem2  31163  3oalem2  31171  hoaddcl  31266  adjsym  31341  cnvadj  31400  hhcno  31412  hhcnf  31413  nmopub2tALT  31417  unoplin  31428  counop  31429  nmfnleub2  31434  hmoplin  31450  brafnmul  31459  nmlnop0iALT  31503  nmopun  31522  nmophmi  31539  riesz3i  31570  riesz1  31573  cnlnadjlem2  31576  cnlnadjlem6  31580  adjmul  31600  adjadd  31601  bra11  31616  cnvbraval  31618  kbass5  31628  kbass6  31629  leop2  31632  leopadd  31640  leopmuli  31641  leoptri  31644  leopnmid  31646  nmopleid  31647  pj3si  31715  hstel2  31727  cvcon3  31792  dmdmd  31808  dmdbr5  31816  mdsl0  31818  mdslmd1lem1  31833  mdslmd1lem2  31834  mdslmd3i  31840  superpos  31862  chirredlem2  31899  chirredlem3  31900  mdsymlem3  31913  mdsymlem5  31915  mdsymlem6  31916  sumdmdlem  31926  cdjreui  31940  cdj1i  31941  cdj3i  31949  foresf1o  31997  2ndimaxp  32127  abfmpel  32135  fcomptf  32138  fcnvgreu  32153  fdifsuppconst  32166  xrge0infss  32228  xnn0gt0  32237  cycpm2tr  32536  intlidl  32798  rhmpreimaprmidl  32832  lssdimle  32968  mdetpmtr1  33089  cmpcref  33116  xrge0iifcnv  33199  esumcst  33347  hasheuni  33369  esum2dlem  33376  esum2d  33377  sigaclcu2  33404  insiga  33421  unelldsys  33442  measres  33506  measdivcst  33508  volfiniune  33514  ddemeas  33520  sgn3da  33826  actfunsnf1o  33902  fnrelpredd  34378  fineqvac  34383  sconnpi1  34516  cvmsss2  34551  satfv1lem  34639  fmlaomn0  34667  gonarlem  34671  mrsubco  34798  dfon2lem6  35052  hfext  35447  gg-psercn2  35464  elicc3  35505  fnessref  35545  bj-ismooredr2  36294  pibt2  36601  fin2solem  36777  fin2so  36778  lindsenlbs  36786  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem2  36793  poimirlem14  36805  poimirlem25  36816  poimirlem26  36817  poimirlem29  36820  poimirlem30  36821  broucube  36825  heicant  36826  mblfinlem2  36829  mblfinlem3  36830  mblfinlem4  36831  ex-ovoliunnfl  36834  mbfresfi  36837  cnambfre  36839  itg2addnclem  36842  itg2addnclem2  36843  itg2addnc  36845  ftc1anclem3  36866  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  indexdom  36905  filbcmb  36911  fdc  36916  incsequz  36919  metf1o  36926  caures  36931  bndss  36957  ismtycnv  36973  heiborlem1  36982  rrncmslem  37003  isdrngo2  37129  rngoisocnv  37152  unichnidl  37202  erimeq2  37851  ax12eq  38114  ax12el  38115  lshpset2N  38292  pmapglb2N  38945  pmapglb2xN  38946  pclfinN  39074  polval2N  39080  cdleme31fv2  39567  cdleme32fvcl  39614  cdleme48gfv  39711  tendoicl  39970  tendoipl  39971  diaglbN  40229  dochkr1  40652  dochkr1OLDN  40653  evlsvvval  41437  selvcllem5  41456  evlselv  41461  fsuppind  41464  fsuppssind  41467  mhpind  41468  sumcubes  41513  dvdsexpim  41521  zaddcomlem  41626  zmulcomlem  41630  nacsfix  41752  eq0rabdioph  41816  diophren  41853  rencldnfilem  41860  pell1234qrdich  41901  jm2.24  42004  jm2.26lem3  42042  wepwsolem  42086  pwssplit4  42133  isnumbasgrplem3  42149  onexoegt  42295  onov0suclim  42326  cantnfresb  42376  omcl2  42385  ofoaid1  42410  ofoaid2  42411  grumnudlem  43346  cvgdvgrat  43374  ofsubid  43385  bcc0  43401  binomcxplemnn0  43410  uzwo4  44042  fiiuncl  44054  iunincfi  44085  nsstr  44086  rexanuz3  44087  iinssiin  44120  disjrnmpt2  44186  disjinfi  44190  choicefi  44198  fsneq  44204  difmap  44205  iunmapsn  44215  axccdom  44220  axccd  44227  rnmptlb  44246  rnmptbd2lem  44251  ssfiunibd  44318  supxrgelem  44346  suplesup  44348  xrlexaddrp  44361  xralrple2  44363  infxrunb2  44377  xralrple3  44383  xrralrecnnle  44392  xrralrecnnge  44399  supxrunb3  44408  unb2ltle  44424  rexabslelem  44427  supminfrnmpt  44454  infxrpnf  44455  supminfxr  44473  supminfxr2  44478  xrpnf  44495  pimxrneun  44498  cvgcaule  44501  iooiinicc  44554  ressioosup  44567  iooiinioc  44568  ressiooinf  44569  fsumsupp0  44593  divcnvg  44642  limcrecl  44644  sumnnodd  44645  islpcn  44654  lptre2pt  44655  limcresiooub  44657  limcresioolb  44658  limclner  44666  fnlimfvre  44689  allbutfifvre  44690  climinf3  44731  limsupmnflem  44735  limsupre3uzlem  44750  limsupreuzmpt  44754  climuzlem  44758  climisp  44761  climrescn  44763  climxrrelem  44764  climxrre  44765  climlimsupcex  44784  liminflelimsuplem  44790  limsupgtlem  44792  liminfvalxr  44798  liminfreuzlem  44817  liminfltlem  44819  liminflimsupclim  44822  xlimpnfxnegmnf  44829  liminflbuz2  44830  liminflimsupxrre  44832  cnrefiisplem  44844  xlimmnfvlem2  44848  xlimmnfv  44849  xlimpnfvlem2  44852  xlimpnfv  44853  xlimmnfmpt  44858  xlimpnfmpt  44859  climxlim2lem  44860  dfxlim2v  44862  xlimliminflimsup  44877  cncfuni  44901  icccncfext  44902  cncficcgt0  44903  cncfiooicclem1  44908  cncfiooiccre  44910  dvasinbx  44935  dvdsn1add  44954  dvnmul  44958  dvmptfprodlem  44959  dvnprodlem1  44961  dvnprodlem3  44963  iblspltprt  44988  itgioocnicc  44992  itgspltprt  44994  ismbl3  45001  stirlinglem5  45093  dirker2re  45107  dirkerper  45111  dirkertrigeq  45116  dirkercncflem2  45119  fourierdlem12  45134  fourierdlem15  45137  fourierdlem16  45138  fourierdlem20  45142  fourierdlem21  45143  fourierdlem22  45144  fourierdlem39  45161  fourierdlem40  45162  fourierdlem41  45163  fourierdlem42  45164  fourierdlem46  45167  fourierdlem49  45170  fourierdlem50  45171  fourierdlem57  45178  fourierdlem58  45179  fourierdlem59  45180  fourierdlem64  45185  fourierdlem65  45186  fourierdlem66  45187  fourierdlem68  45189  fourierdlem70  45191  fourierdlem71  45192  fourierdlem73  45194  fourierdlem78  45199  fourierdlem79  45200  fourierdlem80  45201  fourierdlem81  45202  fourierdlem82  45203  fourierdlem83  45204  fourierdlem87  45208  fourierdlem93  45214  fourierdlem95  45216  fourierdlem101  45222  fourierdlem103  45224  fourierdlem104  45225  fourierdlem111  45232  fourierdlem112  45233  sqwvfoura  45243  fourierswlem  45245  elaa2lem  45248  etransclem13  45262  etransclem23  45272  etransclem24  45273  etransclem32  45281  etransclem38  45287  etransclem46  45295  qndenserrnbllem  45309  rrxsnicc  45315  ioorrnopnlem  45319  prsal  45333  intsal  45345  salexct  45349  dfsalgen2  45356  issalnnd  45360  sge0rnre  45379  sge0val  45381  sge0z  45390  sge0revalmpt  45393  sge0tsms  45395  sge0pr  45409  sge0resplit  45421  sge0split  45424  sge0splitmpt  45426  sge0iunmptlemfi  45428  sge0iunmptlemre  45430  sge0fodjrnlem  45431  sge0iunmpt  45433  sge0rpcpnf  45436  sge0ltfirpmpt2  45441  sge0isum  45442  sge0xaddlem1  45448  sge0xaddlem2  45449  sge0pnffsumgt  45457  sge0gtfsumgt  45458  sge0seq  45461  sge0reuz  45462  nnfoctbdjlem  45470  nnfoctbdj  45471  meadjun  45477  meadjiunlem  45480  voliunsge0lem  45487  meaiuninc3v  45499  omeiunltfirp  45534  carageniuncllem2  45537  caratheodorylem1  45541  caratheodorylem2  45542  caratheodory  45543  isomenndlem  45545  isomennd  45546  hoicvr  45563  volicorescl  45568  ovnsubaddlem2  45586  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvle  45615  ovnhoilem2  45617  hspdifhsp  45631  hoiqssbllem2  45638  hoiqssbllem3  45639  hspmbllem2  45642  ovnsubadd2lem  45660  ovolval4lem1  45664  vonvolmbl  45676  vonioo  45697  vonicc  45700  pimrecltpos  45723  issmfle  45760  smflimlem1  45786  smflimlem2  45787  smflimlem6  45791  smfresal  45803  smfrec  45804  smfmullem4  45809  smfpimcc  45823  smflimmpt  45825  smfsuplem1  45826  smfsuplem3  45828  smfsupmpt  45830  smfsupxr  45831  smfinflem  45832  smfinfmpt  45834  smflimsuplem4  45838  smflimsuplem5  45839  smflimsupmpt  45844  smfliminfmpt  45847  fsupdm  45857  finfdm  45861  smonoord  46338  lswn0  46411  poprelb  46491  fmtnoprmfac1  46532  fmtnofac2lem  46535  sbgoldbst  46745  snlindsntorlem  47239  1arymaptf  47415  ipolubdm  47700  ipoglbdm  47703  aacllem  47936