Theorem adantll 710

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ad2antlr  723  ad2ant2l  742  ad2ant2lr  744  ad5ant23  756  ad5ant24  757  ad5ant25  758  3adant1  1128  3ad2antl3  1185  ralcom2  3371  vtocl2d  3548  sbc2iegf  3858  sbcralt  3865  pofun  5605  poinxp  5755  xpdifid  6166  sossfld  6184  preddowncl  6332  tz7.7  6389  onfr  6402  ssimaex  6975  eqfnun  7037  fndmdif  7042  dffo4  7103  fompt  7118  fcompt  7132  fconst2g  7205  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  24683  iccpnfcnv  24689  icccvx  24695  evth  24705  phtpycc  24737  pcohtpylem  24766  lmmbrf  25010  fgcfil  25019  caucfil  25031  cfilres  25044  bcth3  25079  cmscsscms  25121  ovolfioo  25216  ovolficc  25217  voliunlem3  25301  volcn  25355  mbflimsup  25415  mbfi1fseqlem5  25469  itg2seq  25492  bddiblnc  25591  dvnff  25673  dvnadd  25679  cpnord  25685  c1liplem1  25748  plypf1  25961  plyaddlem1  25962  plymullem1  25963  coeeulem  25973  coeidlem  25986  dgrle  25992  dgrnznn  25996  plycjlem  26026  elqaalem3  26070  ulmcaulem  26142  ulmcau  26143  psergf  26160  psercn2  26171  efopn  26402  abscxpbnd  26497  leibpi  26683  isppw2  26855  muinv  26933  bposlem3  27025  gausslemma2dlem4  27108  pntrmax  27303  pntpbnd1  27325  qabvexp  27365  madebday  27631  mulsrid  27808  eqeelen  28429  colinearalglem4  28434  axcgrid  28441  axsegconlem1  28442  axsegconlem3  28444  ax5seglem1  28453  ax5seglem2  28454  ax5seglem9  28462  axcontlem2  28490  cusgrfilem2  28980  vtxdgfisf  29000  usgr2pthlem  29287  uspgrn2crct  29329  crctcshwlkn0  29342  wwlksnext  29414  wwlksnextproplem3  29432  eupth2lem3lem4  29751  frgr3vlem1  29793  frgr3vlem2  29794  3vfriswmgrlem  29797  frgrwopreglem5  29841  numclwwlk3lem2  29904  grpoidinvlem3  30026  grpoidinv  30028  grpoideu  30029  nmoub3i  30293  nmlno0lem  30313  nmlnoubi  30316  ipasslem3  30353  ipblnfi  30375  hvaddsub4  30598  his35  30608  shsel3  30835  chj4  31055  spansncol  31088  chscllem2  31158  5oalem2  31175  3oalem2  31183  hoaddcl  31278  adjsym  31353  cnvadj  31412  hhcno  31424  hhcnf  31425  nmopub2tALT  31429  unoplin  31440  counop  31441  nmfnleub2  31446  hmoplin  31462  brafnmul  31471  nmlnop0iALT  31515  nmopun  31534  nmophmi  31551  riesz3i  31582  riesz1  31585  cnlnadjlem2  31588  cnlnadjlem6  31592  adjmul  31612  adjadd  31613  bra11  31628  cnvbraval  31630  kbass5  31640  kbass6  31641  leop2  31644  leopadd  31652  leopmuli  31653  leoptri  31656  leopnmid  31658  nmopleid  31659  pj3si  31727  hstel2  31739  cvcon3  31804  dmdmd  31820  dmdbr5  31828  mdsl0  31830  mdslmd1lem1  31845  mdslmd1lem2  31846  mdslmd3i  31852  superpos  31874  chirredlem2  31911  chirredlem3  31912  mdsymlem3  31925  mdsymlem5  31927  mdsymlem6  31928  sumdmdlem  31938  cdjreui  31952  cdj1i  31953  cdj3i  31961  foresf1o  32009  2ndimaxp  32139  abfmpel  32147  fcomptf  32150  fcnvgreu  32165  fdifsuppconst  32178  xrge0infss  32240  xnn0gt0  32249  cycpm2tr  32548  intlidl  32810  rhmpreimaprmidl  32844  lssdimle  32980  mdetpmtr1  33101  cmpcref  33128  xrge0iifcnv  33211  esumcst  33359  hasheuni  33381  esum2dlem  33388  esum2d  33389  sigaclcu2  33416  insiga  33433  unelldsys  33454  measres  33518  measdivcst  33520  volfiniune  33526  ddemeas  33532  sgn3da  33838  actfunsnf1o  33914  fnrelpredd  34390  fineqvac  34395  sconnpi1  34528  cvmsss2  34563  satfv1lem  34651  fmlaomn0  34679  gonarlem  34683  mrsubco  34810  dfon2lem6  35064  hfext  35459  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  44041  fiiuncl  44053  iunincfi  44084  nsstr  44085  rexanuz3  44086  iinssiin  44119  disjrnmpt2  44185  disjinfi  44189  choicefi  44197  fsneq  44203  difmap  44204  iunmapsn  44214  axccdom  44219  axccd  44226  rnmptlb  44245  rnmptbd2lem  44250  ssfiunibd  44317  supxrgelem  44345  suplesup  44347  xrlexaddrp  44360  xralrple2  44362  infxrunb2  44376  xralrple3  44382  xrralrecnnle  44391  xrralrecnnge  44398  supxrunb3  44407  unb2ltle  44423  rexabslelem  44426  supminfrnmpt  44453  infxrpnf  44454  supminfxr  44472  supminfxr2  44477  xrpnf  44494  pimxrneun  44497  cvgcaule  44500  iooiinicc  44553  ressioosup  44566  iooiinioc  44567  ressiooinf  44568  fsumsupp0  44592  divcnvg  44641  limcrecl  44643  sumnnodd  44644  islpcn  44653  lptre2pt  44654  limcresiooub  44656  limcresioolb  44657  limclner  44665  fnlimfvre  44688  allbutfifvre  44689  climinf3  44730  limsupmnflem  44734  limsupre3uzlem  44749  limsupreuzmpt  44753  climuzlem  44757  climisp  44760  climrescn  44762  climxrrelem  44763  climxrre  44764  climlimsupcex  44783  liminflelimsuplem  44789  limsupgtlem  44791  liminfvalxr  44797  liminfreuzlem  44816  liminfltlem  44818  liminflimsupclim  44821  xlimpnfxnegmnf  44828  liminflbuz2  44829  liminflimsupxrre  44831  cnrefiisplem  44843  xlimmnfvlem2  44847  xlimmnfv  44848  xlimpnfvlem2  44851  xlimpnfv  44852  xlimmnfmpt  44857  xlimpnfmpt  44858  climxlim2lem  44859  dfxlim2v  44861  xlimliminflimsup  44876  cncfuni  44900  icccncfext  44901  cncficcgt0  44902  cncfiooicclem1  44907  cncfiooiccre  44909  dvasinbx  44934  dvdsn1add  44953  dvnmul  44957  dvmptfprodlem  44958  dvnprodlem1  44960  dvnprodlem3  44962  iblspltprt  44987  itgioocnicc  44991  itgspltprt  44993  ismbl3  45000  stirlinglem5  45092  dirker2re  45106  dirkerper  45110  dirkertrigeq  45115  dirkercncflem2  45118  fourierdlem12  45133  fourierdlem15  45136  fourierdlem16  45137  fourierdlem20  45141  fourierdlem21  45142  fourierdlem22  45143  fourierdlem39  45160  fourierdlem40  45161  fourierdlem41  45162  fourierdlem42  45163  fourierdlem46  45166  fourierdlem49  45169  fourierdlem50  45170  fourierdlem57  45177  fourierdlem58  45178  fourierdlem59  45179  fourierdlem64  45184  fourierdlem65  45185  fourierdlem66  45186  fourierdlem68  45188  fourierdlem70  45190  fourierdlem71  45191  fourierdlem73  45193  fourierdlem78  45198  fourierdlem79  45199  fourierdlem80  45200  fourierdlem81  45201  fourierdlem82  45202  fourierdlem83  45203  fourierdlem87  45207  fourierdlem93  45213  fourierdlem95  45215  fourierdlem101  45221  fourierdlem103  45223  fourierdlem104  45224  fourierdlem111  45231  fourierdlem112  45232  sqwvfoura  45242  fourierswlem  45244  elaa2lem  45247  etransclem13  45261  etransclem23  45271  etransclem24  45272  etransclem32  45280  etransclem38  45286  etransclem46  45294  qndenserrnbllem  45308  rrxsnicc  45314  ioorrnopnlem  45318  prsal  45332  intsal  45344  salexct  45348  dfsalgen2  45355  issalnnd  45359  sge0rnre  45378  sge0val  45380  sge0z  45389  sge0revalmpt  45392  sge0tsms  45394  sge0pr  45408  sge0resplit  45420  sge0split  45423  sge0splitmpt  45425  sge0iunmptlemfi  45427  sge0iunmptlemre  45429  sge0fodjrnlem  45430  sge0iunmpt  45432  sge0rpcpnf  45435  sge0ltfirpmpt2  45440  sge0isum  45441  sge0xaddlem1  45447  sge0xaddlem2  45448  sge0pnffsumgt  45456  sge0gtfsumgt  45457  sge0seq  45460  sge0reuz  45461  nnfoctbdjlem  45469  nnfoctbdj  45470  meadjun  45476  meadjiunlem  45479  voliunsge0lem  45486  meaiuninc3v  45498  omeiunltfirp  45533  carageniuncllem2  45536  caratheodorylem1  45540  caratheodorylem2  45541  caratheodory  45542  isomenndlem  45544  isomennd  45545  hoicvr  45562  volicorescl  45567  ovnsubaddlem2  45585  hoidmvlelem2  45610  hoidmvlelem3  45611  hoidmvle  45614  ovnhoilem2  45616  hspdifhsp  45630  hoiqssbllem2  45637  hoiqssbllem3  45638  hspmbllem2  45641  ovnsubadd2lem  45659  ovolval4lem1  45663  vonvolmbl  45675  vonioo  45696  vonicc  45699  pimrecltpos  45722  issmfle  45759  smflimlem1  45785  smflimlem2  45786  smflimlem6  45790  smfresal  45802  smfrec  45803  smfmullem4  45808  smfpimcc  45822  smflimmpt  45824  smfsuplem1  45825  smfsuplem3  45827  smfsupmpt  45829  smfsupxr  45830  smfinflem  45831  smfinfmpt  45833  smflimsuplem4  45837  smflimsuplem5  45838  smflimsupmpt  45843  smfliminfmpt  45846  fsupdm  45856  finfdm  45860  smonoord  46337  lswn0  46410  poprelb  46490  fmtnoprmfac1  46531  fmtnofac2lem  46534  sbgoldbst  46744  snlindsntorlem  47238  1arymaptf  47414  ipolubdm  47699  ipoglbdm  47702  aacllem  47935