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  3356  vtocl2d  3541  sbc2iegf  3840  sbcralt  3847  pofun  5579  poinxp  5735  xpdifid  6157  sossfld  6175  preddowncl  6321  tz7.7  6378  onfr  6391  ssimaex  6963  eqfnun  7026  fndmdif  7031  dffo4  7092  fompt  7107  fcompt  7122  fconst2g  7194  f1cofveqaeq  7249  isores3  7327  fvmptopabOLD  7460  limsssuc  7843  el2mpocl  8083  1stconst  8097  2ndconst  8098  curry1  8101  curry2  8104  poseq  8155  soseq  8156  extmptsuppeq  8185  suppss  8191  suppss2  8197  onnseq  8356  oe0  8532  oesuclem  8535  oecl  8547  oaordi  8556  oawordri  8560  omordi  8576  omword2  8584  omlimcl  8588  odi  8589  omass  8590  oeoe  8609  nnaordi  8628  oaabs  8658  omsmolem  8667  eceqoveq  8834  mapsnd  8898  dom2lem  9004  sbthlem9  9103  rexdif1en  9170  php3OLD  9231  onomeneqOLD  9236  isinf  9266  isinfOLD  9267  frfi  9291  fiint  9336  fiintOLD  9337  fodomfib  9339  fodomfibOLD  9341  fofinf1o  9342  marypha1lem  9443  ordiso2  9527  unwdomg  9596  xpwdomg  9597  frr1  9771  ac5num  10048  cff1  10270  cfcoflem  10284  infpssrlem4  10318  isf32lem9  10373  isf34lem7  10391  fin1a2lem13  10424  fin1a2s  10426  hsmexlem4  10441  axdc2lem  10460  zorn2lem6  10513  axpowndlem2  10610  inttsk  10786  tskuni  10795  nqereu  10941  prcdnq  11005  addclprlem2  11029  ltexpri  11055  prlem936  11059  reclem2pr  11060  axsup  11308  add4  11454  ltleadd  11718  lt2mul2div  12118  nn2ge  12265  zextle  12664  fnn0ind  12690  xrlttr  13154  ifle  13211  xnn0lem1lt  13258  xaddass  13263  xmulasslem3  13300  xlemul1a  13302  xadddilem  13308  xrsupsslem  13321  xrinfmsslem  13322  supxrunb1  13333  supxrunb2  13334  ixxin  13377  difreicc  13499  iccsplit  13500  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  fzaddel  13573  fzadd2  13574  fzrev  13602  modadd1  13923  modmul1  13940  fsuppmapnn0fiub  14007  mulexp  14117  expadd  14120  expmul  14123  expnbnd  14248  bccl  14338  hashdom  14395  prsshashgt1  14426  hashfacen  14470  brfi1uzind  14524  wrdnval  14561  swrdccat3blem  14755  revccat  14782  2shfti  15097  rexico  15370  cau3lem  15371  subcn2  15609  caucvgb  15694  iseraltlem1  15696  sumss  15738  fsumsplitsn  15758  incexclem  15850  supcvg  15870  mertenslem2  15899  fprodn0  15993  fprodsplitsn  16003  fprodle  16010  eftlcl  16123  reeftlcl  16124  rpnnen2lem6  16235  dvdsext  16338  3dvds  16348  sqoddm1div8z  16371  gcdcllem3  16518  dvdsexpim  16572  bezoutr1  16586  seq1st  16588  dvdslcm  16615  lcmeq0  16617  lcmcl  16618  lcmneg  16620  lcmdvds  16625  coprmgcdb  16666  dvdsprime  16704  pc2dvds  16897  prmpwdvds  16922  unbenlem  16926  infpnlem1  16928  1arith  16945  vdwmc2  16997  ramcl  17047  mrcuni  17631  isacs1i  17667  acsfn  17669  funcpropd  17913  curfcl  18242  curf2ndf  18257  resmgmhm  18687  resmgmhm2b  18689  mgmhmco  18690  mgmhmima  18691  resmhm  18796  resmhm2b  18798  mhmco  18799  pwsdiagmhm  18807  gsumwsubmcl  18813  gsumwspan  18822  pwmnd  18913  dfgrp2  18943  subgint  19131  ghmmhmb  19208  resghm  19213  cntzmhm  19322  symgextf1lem  19399  f1omvdconj  19425  dfod2  19543  gexdvds  19563  subgpgp  19576  sylow1lem3  19579  frgpnabllem1  19852  dprdfeq0  20003  rhmimasubrnglem  20523  cntzsubrng  20525  cntzsubr  20564  isdrng2  20701  islmodd  20821  lsslss  20916  reslmhm2b  21010  rngqiprngimfo  21260  psgnfix1  21556  psgndif  21560  copsgndif  21561  ocvocv  21629  frlmsslsp  21754  frlmlbs  21755  psrbaglefi  21884  psrdi  21923  psrass23l  21925  psrass23  21927  psdmul  22102  mptcoe1fsupp  22149  psropprmul  22171  ply1coe  22234  rhmcomulmpl  22318  mamudi  22339  mamudir  22340  mat1dimelbas  22407  scmatmulcl  22454  scmatfo  22466  mulmarep1gsum2  22510  mdetunilem7  22554  mdetunilem9  22556  gsummatr01lem3  22593  smadiadetlem3  22604  cpmadugsumlemF  22812  leordtval  23149  cnpnei  23200  cnco  23202  cnss1  23212  cmpsub  23336  hauscmplem  23342  dissnlocfin  23465  ptbasid  23511  tx2cn  23546  upxp  23559  txindis  23570  xkoptsub  23590  xkopt  23591  trfbas2  23779  filconn  23819  trfil2  23823  filssufilg  23847  ufileu  23855  fixufil  23858  ufilen  23866  rnelfmlem  23888  flimclsi  23914  hauspwpwf1  23923  fclsopn  23950  fclsfnflim  23963  fclscmpi  23965  alexsubALTlem4  23986  ptcmplem5  23992  tgpmulg  24029  subgtgp  24041  tgpt0  24055  tsmsxplem2  24090  metss  24445  metustfbas  24494  dscopn  24510  xrsmopn  24750  cncfss  24841  icoopnst  24885  iccpnfcnv  24891  icccvx  24897  evth  24907  phtpycc  24939  pcohtpylem  24968  lmmbrf  25212  fgcfil  25221  caucfil  25233  cfilres  25246  bcth3  25281  cmscsscms  25323  ovolfioo  25418  ovolficc  25419  voliunlem3  25503  volcn  25557  mbflimsup  25617  mbfi1fseqlem5  25670  itg2seq  25693  bddiblnc  25793  dvnff  25875  dvnadd  25881  cpnord  25887  c1liplem1  25951  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coeidlem  26192  dgrle  26198  dgrnznn  26202  plycjlem  26232  elqaalem3  26279  ulmcaulem  26353  ulmcau  26354  psergf  26371  psercn2  26382  psercn2OLD  26383  efopn  26617  abscxpbnd  26713  leibpi  26902  isppw2  27075  muinv  27153  bposlem3  27247  gausslemma2dlem4  27330  pntrmax  27525  pntpbnd1  27547  qabvexp  27587  madebday  27855  mulsrid  28056  peano5n0s  28241  zs12bday  28341  eqeelen  28829  colinearalglem4  28834  axcgrid  28841  axsegconlem1  28842  axsegconlem3  28844  ax5seglem1  28853  ax5seglem2  28854  ax5seglem9  28862  axcontlem2  28890  cusgrfilem2  29382  vtxdgfisf  29402  usgr2pthlem  29691  uspgrn2crct  29736  crctcshwlkn0  29749  wwlksnext  29821  wwlksnextproplem3  29839  eupth2lem3lem4  30158  frgr3vlem1  30200  frgr3vlem2  30201  3vfriswmgrlem  30204  frgrwopreglem5  30248  numclwwlk3lem2  30311  grpoidinvlem3  30433  grpoidinv  30435  grpoideu  30436  nmoub3i  30700  nmlno0lem  30720  nmlnoubi  30723  ipasslem3  30760  ipblnfi  30782  hvaddsub4  31005  his35  31015  shsel3  31242  chj4  31462  spansncol  31495  chscllem2  31565  5oalem2  31582  3oalem2  31590  hoaddcl  31685  adjsym  31760  cnvadj  31819  hhcno  31831  hhcnf  31832  nmopub2tALT  31836  unoplin  31847  counop  31848  nmfnleub2  31853  hmoplin  31869  brafnmul  31878  nmlnop0iALT  31922  nmopun  31941  nmophmi  31958  riesz3i  31989  riesz1  31992  cnlnadjlem2  31995  cnlnadjlem6  31999  adjmul  32019  adjadd  32020  bra11  32035  cnvbraval  32037  kbass5  32047  kbass6  32048  leop2  32051  leopadd  32059  leopmuli  32060  leoptri  32063  leopnmid  32065  nmopleid  32066  pj3si  32134  hstel2  32146  cvcon3  32211  dmdmd  32227  dmdbr5  32235  mdsl0  32237  mdslmd1lem1  32252  mdslmd1lem2  32253  mdslmd3i  32259  superpos  32281  chirredlem2  32318  chirredlem3  32319  mdsymlem3  32332  mdsymlem5  32334  mdsymlem6  32335  sumdmdlem  32345  cdjreui  32359  cdj1i  32360  cdj3i  32368  foresf1o  32431  2ndimaxp  32570  abfmpel  32579  fcomptf  32582  fcnvgreu  32597  fdifsuppconst  32612  xrge0infss  32683  xnn0gt0  32692  sgn3da  32759  cycpm2tr  33076  elrgspnlem2  33184  elrgspnlem3  33185  intlidl  33381  rhmpreimaprmidl  33412  lssdimle  33593  mdetpmtr1  33800  cmpcref  33827  xrge0iifcnv  33910  zrhcntr  33956  esumcst  34040  hasheuni  34062  esum2dlem  34069  esum2d  34070  sigaclcu2  34097  insiga  34114  unelldsys  34135  measres  34199  measdivcst  34201  volfiniune  34207  ddemeas  34213  actfunsnf1o  34582  fnrelpredd  35066  fineqvac  35074  sconnpi1  35207  cvmsss2  35242  satfv1lem  35330  fmlaomn0  35358  gonarlem  35362  mrsubco  35489  dfon2lem6  35752  hfext  36147  elicc3  36281  fnessref  36321  bj-ismooredr2  37074  pibt2  37381  fin2solem  37576  fin2so  37577  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem2  37592  poimirlem14  37604  poimirlem25  37615  poimirlem26  37616  poimirlem29  37619  poimirlem30  37620  broucube  37624  heicant  37625  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ex-ovoliunnfl  37633  mbfresfi  37636  cnambfre  37638  itg2addnclem  37641  itg2addnclem2  37642  itg2addnc  37644  ftc1anclem3  37665  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  indexdom  37704  filbcmb  37710  fdc  37715  incsequz  37718  metf1o  37725  caures  37730  bndss  37756  ismtycnv  37772  heiborlem1  37781  rrncmslem  37802  isdrngo2  37928  rngoisocnv  37951  unichnidl  38001  erimeq2  38642  ax12eq  38905  ax12el  38906  lshpset2N  39083  pmapglb2N  39736  pmapglb2xN  39737  pclfinN  39865  polval2N  39871  cdleme31fv2  40358  cdleme32fvcl  40405  cdleme48gfv  40502  tendoicl  40761  tendoipl  40762  diaglbN  41020  dochkr1  41443  dochkr1OLDN  41444  sumcubes  42309  expeq1d  42320  zaddcomlem  42441  zmulcomlem  42445  fiabv  42506  rhmcomulpsr  42521  evlsvvval  42533  selvcllem5  42552  evlselv  42557  fsuppind  42560  fsuppssind  42563  mhpind  42564  nacsfix  42682  eq0rabdioph  42746  diophren  42783  rencldnfilem  42790  pell1234qrdich  42831  jm2.24  42934  jm2.26lem3  42972  wepwsolem  43013  pwssplit4  43060  isnumbasgrplem3  43076  onexoegt  43215  onov0suclim  43245  cantnfresb  43295  omcl2  43304  ofoaid1  43329  ofoaid2  43330  grumnudlem  44257  cvgdvgrat  44285  ofsubid  44296  bcc0  44312  binomcxplemnn0  44321  uzwo4  45025  fiiuncl  45037  iunincfi  45066  nsstr  45067  rexanuz3  45068  iinssiin  45101  disjrnmpt2  45160  disjinfi  45164  choicefi  45172  fsneq  45178  difmap  45179  iunmapsn  45189  axccdom  45194  axccd  45201  rnmptlb  45215  rnmptbd2lem  45220  ssfiunibd  45286  supxrgelem  45312  suplesup  45314  xrlexaddrp  45327  xralrple2  45329  infxrunb2  45343  xralrple3  45349  xrralrecnnle  45358  xrralrecnnge  45365  supxrunb3  45374  unb2ltle  45390  rexabslelem  45393  supminfrnmpt  45420  infxrpnf  45421  supminfxr  45439  supminfxr2  45444  xrpnf  45460  pimxrneun  45463  cvgcaule  45466  iooiinicc  45519  ressioosup  45532  iooiinioc  45533  ressiooinf  45534  fsumsupp0  45555  divcnvg  45604  limcrecl  45606  sumnnodd  45607  islpcn  45616  lptre2pt  45617  limcresiooub  45619  limcresioolb  45620  limclner  45628  fnlimfvre  45651  allbutfifvre  45652  climinf3  45693  limsupmnflem  45697  limsupre3uzlem  45712  limsupreuzmpt  45716  climuzlem  45720  climisp  45723  climrescn  45725  climxrrelem  45726  climxrre  45727  climlimsupcex  45746  liminflelimsuplem  45752  limsupgtlem  45754  liminfvalxr  45760  liminfreuzlem  45779  liminfltlem  45781  liminflimsupclim  45784  xlimpnfxnegmnf  45791  liminflbuz2  45792  liminflimsupxrre  45794  cnrefiisplem  45806  xlimmnfvlem2  45810  xlimmnfv  45811  xlimpnfvlem2  45814  xlimpnfv  45815  xlimmnfmpt  45820  xlimpnfmpt  45821  climxlim2lem  45822  dfxlim2v  45824  xlimliminflimsup  45839  cncfuni  45863  icccncfext  45864  cncficcgt0  45865  cncfiooicclem1  45870  cncfiooiccre  45872  dvasinbx  45897  dvdsn1add  45916  dvnmul  45920  dvmptfprodlem  45921  dvnprodlem1  45923  dvnprodlem3  45925  iblspltprt  45950  itgioocnicc  45954  itgspltprt  45956  ismbl3  45963  stirlinglem5  46055  dirker2re  46069  dirkerper  46073  dirkertrigeq  46078  dirkercncflem2  46081  fourierdlem12  46096  fourierdlem15  46099  fourierdlem16  46100  fourierdlem20  46104  fourierdlem21  46105  fourierdlem22  46106  fourierdlem39  46123  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem46  46129  fourierdlem49  46132  fourierdlem50  46133  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem64  46147  fourierdlem65  46148  fourierdlem66  46149  fourierdlem68  46151  fourierdlem70  46153  fourierdlem71  46154  fourierdlem73  46156  fourierdlem78  46161  fourierdlem79  46162  fourierdlem80  46163  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem87  46170  fourierdlem93  46176  fourierdlem95  46178  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  sqwvfoura  46205  fourierswlem  46207  elaa2lem  46210  etransclem13  46224  etransclem23  46234  etransclem24  46235  etransclem32  46243  etransclem38  46249  etransclem46  46257  qndenserrnbllem  46271  rrxsnicc  46277  ioorrnopnlem  46281  prsal  46295  intsal  46307  salexct  46311  dfsalgen2  46318  issalnnd  46322  sge0rnre  46341  sge0val  46343  sge0z  46352  sge0revalmpt  46355  sge0tsms  46357  sge0pr  46371  sge0resplit  46383  sge0split  46386  sge0splitmpt  46388  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0fodjrnlem  46393  sge0iunmpt  46395  sge0rpcpnf  46398  sge0ltfirpmpt2  46403  sge0isum  46404  sge0xaddlem1  46410  sge0xaddlem2  46411  sge0pnffsumgt  46419  sge0gtfsumgt  46420  sge0seq  46423  sge0reuz  46424  nnfoctbdjlem  46432  nnfoctbdj  46433  meadjun  46439  meadjiunlem  46442  voliunsge0lem  46449  meaiuninc3v  46461  omeiunltfirp  46496  carageniuncllem2  46499  caratheodorylem1  46503  caratheodorylem2  46504  caratheodory  46505  isomenndlem  46507  isomennd  46508  hoicvr  46525  volicorescl  46530  ovnsubaddlem2  46548  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvle  46577  ovnhoilem2  46579  hspdifhsp  46593  hoiqssbllem2  46600  hoiqssbllem3  46601  hspmbllem2  46604  ovnsubadd2lem  46622  ovolval4lem1  46626  vonvolmbl  46638  vonioo  46659  vonicc  46662  pimrecltpos  46685  issmfle  46722  smflimlem1  46748  smflimlem2  46749  smflimlem6  46753  smfresal  46765  smfrec  46766  smfmullem4  46771  smfpimcc  46785  smflimmpt  46787  smfsuplem1  46788  smfsuplem3  46790  smfsupmpt  46792  smfsupxr  46793  smfinflem  46794  smfinfmpt  46796  smflimsuplem4  46800  smflimsuplem5  46801  smflimsupmpt  46806  smfliminfmpt  46809  fsupdm  46819  finfdm  46823  smonoord  47333  lswn0  47406  poprelb  47486  fmtnoprmfac1  47527  fmtnofac2lem  47530  sbgoldbst  47740  isgrim  47843  gpgedgvtx0  48013  snlindsntorlem  48394  1arymaptf  48569  ipolubdm  48909  ipoglbdm  48912  setc1onsubc  49427  aacllem  49613