Theorem adantll 714

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 580	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 207  df-an 396

This theorem is referenced by:  ad2antlr  727  ad2ant2l  746  ad2ant2lr  748  ad5ant23  759  ad5ant24  760  ad5ant25  761  3adant1  1130  3ad2antl3  1188  ralcom2  3342  vtocl2d  3519  sbc2iegf  3819  sbcralt  3826  pofun  5549  poinxp  5704  xpdifid  6121  sossfld  6139  preddowncl  6284  tz7.7  6337  onfr  6350  ssimaex  6912  eqfnun  6975  fndmdif  6980  dffo4  7041  fompt  7056  fcompt  7071  fconst2g  7143  f1cofveqaeq  7198  isores3  7276  limsssuc  7790  el2mpocl  8026  1stconst  8040  2ndconst  8041  curry1  8044  curry2  8047  poseq  8098  soseq  8099  extmptsuppeq  8128  suppss  8134  suppss2  8140  onnseq  8274  oe0  8447  oesuclem  8450  oecl  8462  oaordi  8471  oawordri  8475  omordi  8491  omword2  8499  omlimcl  8503  odi  8504  omass  8505  oeoe  8524  nnaordi  8543  oaabs  8573  omsmolem  8582  eceqoveq  8756  mapsnd  8820  dom2lem  8924  sbthlem9  9019  rexdif1en  9082  isinf  9165  isinfOLD  9166  frfi  9190  fiint  9235  fiintOLD  9236  fodomfib  9238  fodomfibOLD  9240  fofinf1o  9241  marypha1lem  9342  ordiso2  9426  unwdomg  9495  xpwdomg  9496  frr1  9674  ac5num  9949  cff1  10171  cfcoflem  10185  infpssrlem4  10219  isf32lem9  10274  isf34lem7  10292  fin1a2lem13  10325  fin1a2s  10327  hsmexlem4  10342  axdc2lem  10361  zorn2lem6  10414  axpowndlem2  10511  inttsk  10687  tskuni  10696  nqereu  10842  prcdnq  10906  addclprlem2  10930  ltexpri  10956  prlem936  10960  reclem2pr  10961  axsup  11209  add4  11355  ltleadd  11621  lt2mul2div  12021  nn2ge  12173  zextle  12567  fnn0ind  12593  xrlttr  13060  ifle  13117  xnn0lem1lt  13164  xaddass  13169  xmulasslem3  13206  xlemul1a  13208  xadddilem  13214  xrsupsslem  13227  xrinfmsslem  13228  supxrunb1  13239  supxrunb2  13240  ixxin  13283  difreicc  13405  iccsplit  13406  iccshftr  13407  iccshftl  13409  iccdil  13411  icccntr  13413  fzaddel  13479  fzadd2  13480  fzrev  13508  modadd1  13830  modmul1  13849  fsuppmapnn0fiub  13916  mulexp  14026  expadd  14029  expmul  14032  expnbnd  14157  bccl  14247  hashdom  14304  prsshashgt1  14335  hashfacen  14379  brfi1uzind  14433  wrdnval  14470  swrdccat3blem  14663  revccat  14690  2shfti  15005  rexico  15279  cau3lem  15280  subcn2  15520  caucvgb  15605  iseraltlem1  15607  sumss  15649  fsumsplitsn  15669  incexclem  15761  supcvg  15781  mertenslem2  15810  fprodn0  15904  fprodsplitsn  15914  fprodle  15921  eftlcl  16034  reeftlcl  16035  rpnnen2lem6  16146  dvdsext  16250  3dvds  16260  sqoddm1div8z  16283  gcdcllem3  16430  dvdsexpim  16484  bezoutr1  16498  seq1st  16500  dvdslcm  16527  lcmeq0  16529  lcmcl  16530  lcmneg  16532  lcmdvds  16537  coprmgcdb  16578  dvdsprime  16616  pc2dvds  16809  prmpwdvds  16834  unbenlem  16838  infpnlem1  16840  1arith  16857  vdwmc2  16909  ramcl  16959  mrcuni  17545  isacs1i  17581  acsfn  17583  funcpropd  17827  curfcl  18156  curf2ndf  18171  resmgmhm  18603  resmgmhm2b  18605  mgmhmco  18606  mgmhmima  18607  resmhm  18712  resmhm2b  18714  mhmco  18715  pwsdiagmhm  18723  gsumwsubmcl  18729  gsumwspan  18738  pwmnd  18829  dfgrp2  18859  subgint  19047  ghmmhmb  19124  resghm  19129  cntzmhm  19238  symgextf1lem  19317  f1omvdconj  19343  dfod2  19461  gexdvds  19481  subgpgp  19494  sylow1lem3  19497  frgpnabllem1  19770  dprdfeq0  19921  rhmimasubrnglem  20468  cntzsubrng  20470  cntzsubr  20509  isdrng2  20646  islmodd  20787  lsslss  20882  reslmhm2b  20976  rngqiprngimfo  21226  psgnfix1  21523  psgndif  21527  copsgndif  21528  ocvocv  21596  frlmsslsp  21721  frlmlbs  21722  psrbaglefi  21851  psrdi  21890  psrass23l  21892  psrass23  21894  psdmul  22069  mptcoe1fsupp  22116  psropprmul  22138  ply1coe  22201  rhmcomulmpl  22285  mamudi  22306  mamudir  22307  mat1dimelbas  22374  scmatmulcl  22421  scmatfo  22433  mulmarep1gsum2  22477  mdetunilem7  22521  mdetunilem9  22523  gsummatr01lem3  22560  smadiadetlem3  22571  cpmadugsumlemF  22779  leordtval  23116  cnpnei  23167  cnco  23169  cnss1  23179  cmpsub  23303  hauscmplem  23309  dissnlocfin  23432  ptbasid  23478  tx2cn  23513  upxp  23526  txindis  23537  xkoptsub  23557  xkopt  23558  trfbas2  23746  filconn  23786  trfil2  23790  filssufilg  23814  ufileu  23822  fixufil  23825  ufilen  23833  rnelfmlem  23855  flimclsi  23881  hauspwpwf1  23890  fclsopn  23917  fclsfnflim  23930  fclscmpi  23932  alexsubALTlem4  23953  ptcmplem5  23959  tgpmulg  23996  subgtgp  24008  tgpt0  24022  tsmsxplem2  24057  metss  24412  metustfbas  24461  dscopn  24477  xrsmopn  24717  cncfss  24808  icoopnst  24852  iccpnfcnv  24858  icccvx  24864  evth  24874  phtpycc  24906  pcohtpylem  24935  lmmbrf  25178  fgcfil  25187  caucfil  25199  cfilres  25212  bcth3  25247  cmscsscms  25289  ovolfioo  25384  ovolficc  25385  voliunlem3  25469  volcn  25523  mbflimsup  25583  mbfi1fseqlem5  25636  itg2seq  25659  bddiblnc  25759  dvnff  25841  dvnadd  25847  cpnord  25853  c1liplem1  25917  plypf1  26133  plyaddlem1  26134  plymullem1  26135  coeeulem  26145  coeidlem  26158  dgrle  26164  dgrnznn  26168  plycjlem  26198  elqaalem3  26245  ulmcaulem  26319  ulmcau  26320  psergf  26337  psercn2  26348  psercn2OLD  26349  efopn  26583  abscxpbnd  26679  leibpi  26868  isppw2  27041  muinv  27119  bposlem3  27213  gausslemma2dlem4  27296  pntrmax  27491  pntpbnd1  27513  qabvexp  27553  madebday  27832  mulsrid  28039  bdayon  28196  peano5n0s  28235  zs12bday  28379  eqeelen  28867  colinearalglem4  28872  axcgrid  28879  axsegconlem1  28880  axsegconlem3  28882  ax5seglem1  28891  ax5seglem2  28892  ax5seglem9  28900  axcontlem2  28928  cusgrfilem2  29420  vtxdgfisf  29440  usgr2pthlem  29726  uspgrn2crct  29771  crctcshwlkn0  29784  wwlksnext  29856  wwlksnextproplem3  29874  eupth2lem3lem4  30193  frgr3vlem1  30235  frgr3vlem2  30236  3vfriswmgrlem  30239  frgrwopreglem5  30283  numclwwlk3lem2  30346  grpoidinvlem3  30468  grpoidinv  30470  grpoideu  30471  nmoub3i  30735  nmlno0lem  30755  nmlnoubi  30758  ipasslem3  30795  ipblnfi  30817  hvaddsub4  31040  his35  31050  shsel3  31277  chj4  31497  spansncol  31530  chscllem2  31600  5oalem2  31617  3oalem2  31625  hoaddcl  31720  adjsym  31795  cnvadj  31854  hhcno  31866  hhcnf  31867  nmopub2tALT  31871  unoplin  31882  counop  31883  nmfnleub2  31888  hmoplin  31904  brafnmul  31913  nmlnop0iALT  31957  nmopun  31976  nmophmi  31993  riesz3i  32024  riesz1  32027  cnlnadjlem2  32030  cnlnadjlem6  32034  adjmul  32054  adjadd  32055  bra11  32070  cnvbraval  32072  kbass5  32082  kbass6  32083  leop2  32086  leopadd  32094  leopmuli  32095  leoptri  32098  leopnmid  32100  nmopleid  32101  pj3si  32169  hstel2  32181  cvcon3  32246  dmdmd  32262  dmdbr5  32270  mdsl0  32272  mdslmd1lem1  32287  mdslmd1lem2  32288  mdslmd3i  32294  superpos  32316  chirredlem2  32353  chirredlem3  32354  mdsymlem3  32367  mdsymlem5  32369  mdsymlem6  32370  sumdmdlem  32380  cdjreui  32394  cdj1i  32395  cdj3i  32403  foresf1o  32466  2ndimaxp  32603  abfmpel  32612  fcomptf  32615  fcnvgreu  32630  fdifsuppconst  32645  xrge0infss  32716  xnn0gt0  32725  sgn3da  32792  cycpm2tr  33074  elrgspnlem2  33196  elrgspnlem3  33197  intlidl  33370  rhmpreimaprmidl  33401  lssdimle  33582  mdetpmtr1  33792  cmpcref  33819  xrge0iifcnv  33902  zrhcntr  33948  esumcst  34032  hasheuni  34054  esum2dlem  34061  esum2d  34062  sigaclcu2  34089  insiga  34106  unelldsys  34127  measres  34191  measdivcst  34193  volfiniune  34199  ddemeas  34205  actfunsnf1o  34574  fnrelpredd  35058  fineqvac  35074  sconnpi1  35214  cvmsss2  35249  satfv1lem  35337  fmlaomn0  35365  gonarlem  35369  mrsubco  35496  dfon2lem6  35764  hfext  36159  elicc3  36293  fnessref  36333  bj-ismooredr2  37086  pibt2  37393  fin2solem  37588  fin2so  37589  lindsenlbs  37597  matunitlindflem1  37598  matunitlindflem2  37599  poimirlem2  37604  poimirlem14  37616  poimirlem25  37627  poimirlem26  37628  poimirlem29  37631  poimirlem30  37632  broucube  37636  heicant  37637  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  ex-ovoliunnfl  37645  mbfresfi  37648  cnambfre  37650  itg2addnclem  37653  itg2addnclem2  37654  itg2addnc  37656  ftc1anclem3  37677  ftc1anclem4  37678  ftc1anclem5  37679  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  indexdom  37716  filbcmb  37722  fdc  37727  incsequz  37730  metf1o  37737  caures  37742  bndss  37768  ismtycnv  37784  heiborlem1  37793  rrncmslem  37814  isdrngo2  37940  rngoisocnv  37963  unichnidl  38013  erimeq2  38658  ax12eq  38922  ax12el  38923  lshpset2N  39100  pmapglb2N  39753  pmapglb2xN  39754  pclfinN  39882  polval2N  39888  cdleme31fv2  40375  cdleme32fvcl  40422  cdleme48gfv  40519  tendoicl  40778  tendoipl  40779  diaglbN  41037  dochkr1  41460  dochkr1OLDN  41461  sumcubes  42289  expeq1d  42300  zaddcomlem  42439  zmulcomlem  42443  fiabv  42512  rhmcomulpsr  42527  evlsvvval  42539  selvcllem5  42558  evlselv  42563  fsuppind  42566  fsuppssind  42569  mhpind  42570  nacsfix  42688  eq0rabdioph  42752  diophren  42789  rencldnfilem  42796  pell1234qrdich  42837  jm2.24  42939  jm2.26lem3  42977  wepwsolem  43018  pwssplit4  43065  isnumbasgrplem3  43081  onexoegt  43220  onov0suclim  43250  cantnfresb  43300  omcl2  43309  ofoaid1  43334  ofoaid2  43335  grumnudlem  44261  cvgdvgrat  44289  ofsubid  44300  bcc0  44316  binomcxplemnn0  44325  uzwo4  45034  fiiuncl  45046  iunincfi  45075  nsstr  45076  rexanuz3  45077  iinssiin  45110  disjrnmpt2  45169  disjinfi  45173  choicefi  45181  fsneq  45187  difmap  45188  iunmapsn  45198  axccdom  45203  axccd  45210  rnmptlb  45224  rnmptbd2lem  45229  ssfiunibd  45294  supxrgelem  45320  suplesup  45322  xrlexaddrp  45335  xralrple2  45337  infxrunb2  45351  xralrple3  45357  xrralrecnnle  45366  xrralrecnnge  45373  supxrunb3  45382  unb2ltle  45398  rexabslelem  45401  supminfrnmpt  45428  infxrpnf  45429  supminfxr  45447  supminfxr2  45452  xrpnf  45468  pimxrneun  45471  cvgcaule  45474  iooiinicc  45527  ressioosup  45540  iooiinioc  45541  ressiooinf  45542  fsumsupp0  45563  divcnvg  45612  limcrecl  45614  sumnnodd  45615  islpcn  45624  lptre2pt  45625  limcresiooub  45627  limcresioolb  45628  limclner  45636  fnlimfvre  45659  allbutfifvre  45660  climinf3  45701  limsupmnflem  45705  limsupre3uzlem  45720  limsupreuzmpt  45724  climuzlem  45728  climisp  45731  climrescn  45733  climxrrelem  45734  climxrre  45735  climlimsupcex  45754  liminflelimsuplem  45760  limsupgtlem  45762  liminfvalxr  45768  liminfreuzlem  45787  liminfltlem  45789  liminflimsupclim  45792  xlimpnfxnegmnf  45799  liminflbuz2  45800  liminflimsupxrre  45802  cnrefiisplem  45814  xlimmnfvlem2  45818  xlimmnfv  45819  xlimpnfvlem2  45822  xlimpnfv  45823  xlimmnfmpt  45828  xlimpnfmpt  45829  climxlim2lem  45830  dfxlim2v  45832  xlimliminflimsup  45847  cncfuni  45871  icccncfext  45872  cncficcgt0  45873  cncfiooicclem1  45878  cncfiooiccre  45880  dvasinbx  45905  dvdsn1add  45924  dvnmul  45928  dvmptfprodlem  45929  dvnprodlem1  45931  dvnprodlem3  45933  iblspltprt  45958  itgioocnicc  45962  itgspltprt  45964  ismbl3  45971  stirlinglem5  46063  dirker2re  46077  dirkerper  46081  dirkertrigeq  46086  dirkercncflem2  46089  fourierdlem12  46104  fourierdlem15  46107  fourierdlem16  46108  fourierdlem20  46112  fourierdlem21  46113  fourierdlem22  46114  fourierdlem39  46131  fourierdlem40  46132  fourierdlem41  46133  fourierdlem42  46134  fourierdlem46  46137  fourierdlem49  46140  fourierdlem50  46141  fourierdlem57  46148  fourierdlem58  46149  fourierdlem59  46150  fourierdlem64  46155  fourierdlem65  46156  fourierdlem66  46157  fourierdlem68  46159  fourierdlem70  46161  fourierdlem71  46162  fourierdlem73  46164  fourierdlem78  46169  fourierdlem79  46170  fourierdlem80  46171  fourierdlem81  46172  fourierdlem82  46173  fourierdlem83  46174  fourierdlem87  46178  fourierdlem93  46184  fourierdlem95  46186  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  fourierdlem112  46203  sqwvfoura  46213  fourierswlem  46215  elaa2lem  46218  etransclem13  46232  etransclem23  46242  etransclem24  46243  etransclem32  46251  etransclem38  46257  etransclem46  46265  qndenserrnbllem  46279  rrxsnicc  46285  ioorrnopnlem  46289  prsal  46303  intsal  46315  salexct  46319  dfsalgen2  46326  issalnnd  46330  sge0rnre  46349  sge0val  46351  sge0z  46360  sge0revalmpt  46363  sge0tsms  46365  sge0pr  46379  sge0resplit  46391  sge0split  46394  sge0splitmpt  46396  sge0iunmptlemfi  46398  sge0iunmptlemre  46400  sge0fodjrnlem  46401  sge0iunmpt  46403  sge0rpcpnf  46406  sge0ltfirpmpt2  46411  sge0isum  46412  sge0xaddlem1  46418  sge0xaddlem2  46419  sge0pnffsumgt  46427  sge0gtfsumgt  46428  sge0seq  46431  sge0reuz  46432  nnfoctbdjlem  46440  nnfoctbdj  46441  meadjun  46447  meadjiunlem  46450  voliunsge0lem  46457  meaiuninc3v  46469  omeiunltfirp  46504  carageniuncllem2  46507  caratheodorylem1  46511  caratheodorylem2  46512  caratheodory  46513  isomenndlem  46515  isomennd  46516  hoicvr  46533  volicorescl  46538  ovnsubaddlem2  46556  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvle  46585  ovnhoilem2  46587  hspdifhsp  46601  hoiqssbllem2  46608  hoiqssbllem3  46609  hspmbllem2  46612  ovnsubadd2lem  46630  ovolval4lem1  46634  vonvolmbl  46646  vonioo  46667  vonicc  46670  pimrecltpos  46693  issmfle  46730  smflimlem1  46756  smflimlem2  46757  smflimlem6  46761  smfresal  46773  smfrec  46774  smfmullem4  46779  smfpimcc  46793  smflimmpt  46795  smfsuplem1  46796  smfsuplem3  46798  smfsupmpt  46800  smfsupxr  46801  smfinflem  46802  smfinfmpt  46804  smflimsuplem4  46808  smflimsuplem5  46809  smflimsupmpt  46814  smfliminfmpt  46817  fsupdm  46827  finfdm  46831  smonoord  47359  lswn0  47432  poprelb  47512  fmtnoprmfac1  47553  fmtnofac2lem  47556  sbgoldbst  47766  isgrim  47870  gpgedgvtx0  48049  snlindsntorlem  48459  1arymaptf  48630  ipolubdm  48975  ipoglbdm  48978  setc1onsubc  49591  aacllem  49790