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  3348  vtocl2d  3525  sbc2iegf  3825  sbcralt  3832  pofun  5557  poinxp  5712  xpdifid  6129  sossfld  6147  preddowncl  6293  tz7.7  6346  onfr  6359  ssimaex  6928  eqfnun  6991  fndmdif  6996  dffo4  7057  fompt  7072  fcompt  7087  fconst2g  7159  f1cofveqaeq  7214  isores3  7292  limsssuc  7806  el2mpocl  8042  1stconst  8056  2ndconst  8057  curry1  8060  curry2  8063  poseq  8114  soseq  8115  extmptsuppeq  8144  suppss  8150  suppss2  8156  onnseq  8290  oe0  8463  oesuclem  8466  oecl  8478  oaordi  8487  oawordri  8491  omordi  8507  omword2  8515  omlimcl  8519  odi  8520  omass  8521  oeoe  8540  nnaordi  8559  oaabs  8589  omsmolem  8598  eceqoveq  8772  mapsnd  8836  dom2lem  8940  sbthlem9  9036  rexdif1en  9099  isinf  9183  isinfOLD  9184  frfi  9208  fiint  9253  fiintOLD  9254  fodomfib  9256  fodomfibOLD  9258  fofinf1o  9259  marypha1lem  9360  ordiso2  9444  unwdomg  9513  xpwdomg  9514  frr1  9688  ac5num  9965  cff1  10187  cfcoflem  10201  infpssrlem4  10235  isf32lem9  10290  isf34lem7  10308  fin1a2lem13  10341  fin1a2s  10343  hsmexlem4  10358  axdc2lem  10377  zorn2lem6  10430  axpowndlem2  10527  inttsk  10703  tskuni  10712  nqereu  10858  prcdnq  10922  addclprlem2  10946  ltexpri  10972  prlem936  10976  reclem2pr  10977  axsup  11225  add4  11371  ltleadd  11637  lt2mul2div  12037  nn2ge  12189  zextle  12583  fnn0ind  12609  xrlttr  13076  ifle  13133  xnn0lem1lt  13180  xaddass  13185  xmulasslem3  13222  xlemul1a  13224  xadddilem  13230  xrsupsslem  13243  xrinfmsslem  13244  supxrunb1  13255  supxrunb2  13256  ixxin  13299  difreicc  13421  iccsplit  13422  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  fzaddel  13495  fzadd2  13496  fzrev  13524  modadd1  13846  modmul1  13865  fsuppmapnn0fiub  13932  mulexp  14042  expadd  14045  expmul  14048  expnbnd  14173  bccl  14263  hashdom  14320  prsshashgt1  14351  hashfacen  14395  brfi1uzind  14449  wrdnval  14486  swrdccat3blem  14680  revccat  14707  2shfti  15022  rexico  15296  cau3lem  15297  subcn2  15537  caucvgb  15622  iseraltlem1  15624  sumss  15666  fsumsplitsn  15686  incexclem  15778  supcvg  15798  mertenslem2  15827  fprodn0  15921  fprodsplitsn  15931  fprodle  15938  eftlcl  16051  reeftlcl  16052  rpnnen2lem6  16163  dvdsext  16267  3dvds  16277  sqoddm1div8z  16300  gcdcllem3  16447  dvdsexpim  16501  bezoutr1  16515  seq1st  16517  dvdslcm  16544  lcmeq0  16546  lcmcl  16547  lcmneg  16549  lcmdvds  16554  coprmgcdb  16595  dvdsprime  16633  pc2dvds  16826  prmpwdvds  16851  unbenlem  16855  infpnlem1  16857  1arith  16874  vdwmc2  16926  ramcl  16976  mrcuni  17558  isacs1i  17594  acsfn  17596  funcpropd  17840  curfcl  18169  curf2ndf  18184  resmgmhm  18614  resmgmhm2b  18616  mgmhmco  18617  mgmhmima  18618  resmhm  18723  resmhm2b  18725  mhmco  18726  pwsdiagmhm  18734  gsumwsubmcl  18740  gsumwspan  18749  pwmnd  18840  dfgrp2  18870  subgint  19058  ghmmhmb  19135  resghm  19140  cntzmhm  19249  symgextf1lem  19326  f1omvdconj  19352  dfod2  19470  gexdvds  19490  subgpgp  19503  sylow1lem3  19506  frgpnabllem1  19779  dprdfeq0  19930  rhmimasubrnglem  20450  cntzsubrng  20452  cntzsubr  20491  isdrng2  20628  islmodd  20748  lsslss  20843  reslmhm2b  20937  rngqiprngimfo  21187  psgnfix1  21483  psgndif  21487  copsgndif  21488  ocvocv  21556  frlmsslsp  21681  frlmlbs  21682  psrbaglefi  21811  psrdi  21850  psrass23l  21852  psrass23  21854  psdmul  22029  mptcoe1fsupp  22076  psropprmul  22098  ply1coe  22161  rhmcomulmpl  22245  mamudi  22266  mamudir  22267  mat1dimelbas  22334  scmatmulcl  22381  scmatfo  22393  mulmarep1gsum2  22437  mdetunilem7  22481  mdetunilem9  22483  gsummatr01lem3  22520  smadiadetlem3  22531  cpmadugsumlemF  22739  leordtval  23076  cnpnei  23127  cnco  23129  cnss1  23139  cmpsub  23263  hauscmplem  23269  dissnlocfin  23392  ptbasid  23438  tx2cn  23473  upxp  23486  txindis  23497  xkoptsub  23517  xkopt  23518  trfbas2  23706  filconn  23746  trfil2  23750  filssufilg  23774  ufileu  23782  fixufil  23785  ufilen  23793  rnelfmlem  23815  flimclsi  23841  hauspwpwf1  23850  fclsopn  23877  fclsfnflim  23890  fclscmpi  23892  alexsubALTlem4  23913  ptcmplem5  23919  tgpmulg  23956  subgtgp  23968  tgpt0  23982  tsmsxplem2  24017  metss  24372  metustfbas  24421  dscopn  24437  xrsmopn  24677  cncfss  24768  icoopnst  24812  iccpnfcnv  24818  icccvx  24824  evth  24834  phtpycc  24866  pcohtpylem  24895  lmmbrf  25138  fgcfil  25147  caucfil  25159  cfilres  25172  bcth3  25207  cmscsscms  25249  ovolfioo  25344  ovolficc  25345  voliunlem3  25429  volcn  25483  mbflimsup  25543  mbfi1fseqlem5  25596  itg2seq  25619  bddiblnc  25719  dvnff  25801  dvnadd  25807  cpnord  25813  c1liplem1  25877  plypf1  26093  plyaddlem1  26094  plymullem1  26095  coeeulem  26105  coeidlem  26118  dgrle  26124  dgrnznn  26128  plycjlem  26158  elqaalem3  26205  ulmcaulem  26279  ulmcau  26280  psergf  26297  psercn2  26308  psercn2OLD  26309  efopn  26543  abscxpbnd  26639  leibpi  26828  isppw2  27001  muinv  27079  bposlem3  27173  gausslemma2dlem4  27256  pntrmax  27451  pntpbnd1  27473  qabvexp  27513  madebday  27787  mulsrid  27992  bdayon  28149  peano5n0s  28188  zs12bday  28319  eqeelen  28807  colinearalglem4  28812  axcgrid  28819  axsegconlem1  28820  axsegconlem3  28822  ax5seglem1  28831  ax5seglem2  28832  ax5seglem9  28840  axcontlem2  28868  cusgrfilem2  29360  vtxdgfisf  29380  usgr2pthlem  29666  uspgrn2crct  29711  crctcshwlkn0  29724  wwlksnext  29796  wwlksnextproplem3  29814  eupth2lem3lem4  30133  frgr3vlem1  30175  frgr3vlem2  30176  3vfriswmgrlem  30179  frgrwopreglem5  30223  numclwwlk3lem2  30286  grpoidinvlem3  30408  grpoidinv  30410  grpoideu  30411  nmoub3i  30675  nmlno0lem  30695  nmlnoubi  30698  ipasslem3  30735  ipblnfi  30757  hvaddsub4  30980  his35  30990  shsel3  31217  chj4  31437  spansncol  31470  chscllem2  31540  5oalem2  31557  3oalem2  31565  hoaddcl  31660  adjsym  31735  cnvadj  31794  hhcno  31806  hhcnf  31807  nmopub2tALT  31811  unoplin  31822  counop  31823  nmfnleub2  31828  hmoplin  31844  brafnmul  31853  nmlnop0iALT  31897  nmopun  31916  nmophmi  31933  riesz3i  31964  riesz1  31967  cnlnadjlem2  31970  cnlnadjlem6  31974  adjmul  31994  adjadd  31995  bra11  32010  cnvbraval  32012  kbass5  32022  kbass6  32023  leop2  32026  leopadd  32034  leopmuli  32035  leoptri  32038  leopnmid  32040  nmopleid  32041  pj3si  32109  hstel2  32121  cvcon3  32186  dmdmd  32202  dmdbr5  32210  mdsl0  32212  mdslmd1lem1  32227  mdslmd1lem2  32228  mdslmd3i  32234  superpos  32256  chirredlem2  32293  chirredlem3  32294  mdsymlem3  32307  mdsymlem5  32309  mdsymlem6  32310  sumdmdlem  32320  cdjreui  32334  cdj1i  32335  cdj3i  32343  foresf1o  32406  2ndimaxp  32543  abfmpel  32552  fcomptf  32555  fcnvgreu  32570  fdifsuppconst  32585  xrge0infss  32656  xnn0gt0  32665  sgn3da  32732  cycpm2tr  33049  elrgspnlem2  33167  elrgspnlem3  33168  intlidl  33364  rhmpreimaprmidl  33395  lssdimle  33576  mdetpmtr1  33786  cmpcref  33813  xrge0iifcnv  33896  zrhcntr  33942  esumcst  34026  hasheuni  34048  esum2dlem  34055  esum2d  34056  sigaclcu2  34083  insiga  34100  unelldsys  34121  measres  34185  measdivcst  34187  volfiniune  34193  ddemeas  34199  actfunsnf1o  34568  fnrelpredd  35052  fineqvac  35060  sconnpi1  35199  cvmsss2  35234  satfv1lem  35322  fmlaomn0  35350  gonarlem  35354  mrsubco  35481  dfon2lem6  35749  hfext  36144  elicc3  36278  fnessref  36318  bj-ismooredr2  37071  pibt2  37378  fin2solem  37573  fin2so  37574  lindsenlbs  37582  matunitlindflem1  37583  matunitlindflem2  37584  poimirlem2  37589  poimirlem14  37601  poimirlem25  37612  poimirlem26  37613  poimirlem29  37616  poimirlem30  37617  broucube  37621  heicant  37622  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ex-ovoliunnfl  37630  mbfresfi  37633  cnambfre  37635  itg2addnclem  37638  itg2addnclem2  37639  itg2addnc  37641  ftc1anclem3  37662  ftc1anclem4  37663  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  indexdom  37701  filbcmb  37707  fdc  37712  incsequz  37715  metf1o  37722  caures  37727  bndss  37753  ismtycnv  37769  heiborlem1  37778  rrncmslem  37799  isdrngo2  37925  rngoisocnv  37948  unichnidl  37998  erimeq2  38643  ax12eq  38907  ax12el  38908  lshpset2N  39085  pmapglb2N  39738  pmapglb2xN  39739  pclfinN  39867  polval2N  39873  cdleme31fv2  40360  cdleme32fvcl  40407  cdleme48gfv  40504  tendoicl  40763  tendoipl  40764  diaglbN  41022  dochkr1  41445  dochkr1OLDN  41446  sumcubes  42274  expeq1d  42285  zaddcomlem  42424  zmulcomlem  42428  fiabv  42497  rhmcomulpsr  42512  evlsvvval  42524  selvcllem5  42543  evlselv  42548  fsuppind  42551  fsuppssind  42554  mhpind  42555  nacsfix  42673  eq0rabdioph  42737  diophren  42774  rencldnfilem  42781  pell1234qrdich  42822  jm2.24  42925  jm2.26lem3  42963  wepwsolem  43004  pwssplit4  43051  isnumbasgrplem3  43067  onexoegt  43206  onov0suclim  43236  cantnfresb  43286  omcl2  43295  ofoaid1  43320  ofoaid2  43321  grumnudlem  44247  cvgdvgrat  44275  ofsubid  44286  bcc0  44302  binomcxplemnn0  44311  uzwo4  45020  fiiuncl  45032  iunincfi  45061  nsstr  45062  rexanuz3  45063  iinssiin  45096  disjrnmpt2  45155  disjinfi  45159  choicefi  45167  fsneq  45173  difmap  45174  iunmapsn  45184  axccdom  45189  axccd  45196  rnmptlb  45210  rnmptbd2lem  45215  ssfiunibd  45280  supxrgelem  45306  suplesup  45308  xrlexaddrp  45321  xralrple2  45323  infxrunb2  45337  xralrple3  45343  xrralrecnnle  45352  xrralrecnnge  45359  supxrunb3  45368  unb2ltle  45384  rexabslelem  45387  supminfrnmpt  45414  infxrpnf  45415  supminfxr  45433  supminfxr2  45438  xrpnf  45454  pimxrneun  45457  cvgcaule  45460  iooiinicc  45513  ressioosup  45526  iooiinioc  45527  ressiooinf  45528  fsumsupp0  45549  divcnvg  45598  limcrecl  45600  sumnnodd  45601  islpcn  45610  lptre2pt  45611  limcresiooub  45613  limcresioolb  45614  limclner  45622  fnlimfvre  45645  allbutfifvre  45646  climinf3  45687  limsupmnflem  45691  limsupre3uzlem  45706  limsupreuzmpt  45710  climuzlem  45714  climisp  45717  climrescn  45719  climxrrelem  45720  climxrre  45721  climlimsupcex  45740  liminflelimsuplem  45746  limsupgtlem  45748  liminfvalxr  45754  liminfreuzlem  45773  liminfltlem  45775  liminflimsupclim  45778  xlimpnfxnegmnf  45785  liminflbuz2  45786  liminflimsupxrre  45788  cnrefiisplem  45800  xlimmnfvlem2  45804  xlimmnfv  45805  xlimpnfvlem2  45808  xlimpnfv  45809  xlimmnfmpt  45814  xlimpnfmpt  45815  climxlim2lem  45816  dfxlim2v  45818  xlimliminflimsup  45833  cncfuni  45857  icccncfext  45858  cncficcgt0  45859  cncfiooicclem1  45864  cncfiooiccre  45866  dvasinbx  45891  dvdsn1add  45910  dvnmul  45914  dvmptfprodlem  45915  dvnprodlem1  45917  dvnprodlem3  45919  iblspltprt  45944  itgioocnicc  45948  itgspltprt  45950  ismbl3  45957  stirlinglem5  46049  dirker2re  46063  dirkerper  46067  dirkertrigeq  46072  dirkercncflem2  46075  fourierdlem12  46090  fourierdlem15  46093  fourierdlem16  46094  fourierdlem20  46098  fourierdlem21  46099  fourierdlem22  46100  fourierdlem39  46117  fourierdlem40  46118  fourierdlem41  46119  fourierdlem42  46120  fourierdlem46  46123  fourierdlem49  46126  fourierdlem50  46127  fourierdlem57  46134  fourierdlem58  46135  fourierdlem59  46136  fourierdlem64  46141  fourierdlem65  46142  fourierdlem66  46143  fourierdlem68  46145  fourierdlem70  46147  fourierdlem71  46148  fourierdlem73  46150  fourierdlem78  46155  fourierdlem79  46156  fourierdlem80  46157  fourierdlem81  46158  fourierdlem82  46159  fourierdlem83  46160  fourierdlem87  46164  fourierdlem93  46170  fourierdlem95  46172  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  sqwvfoura  46199  fourierswlem  46201  elaa2lem  46204  etransclem13  46218  etransclem23  46228  etransclem24  46229  etransclem32  46237  etransclem38  46243  etransclem46  46251  qndenserrnbllem  46265  rrxsnicc  46271  ioorrnopnlem  46275  prsal  46289  intsal  46301  salexct  46305  dfsalgen2  46312  issalnnd  46316  sge0rnre  46335  sge0val  46337  sge0z  46346  sge0revalmpt  46349  sge0tsms  46351  sge0pr  46365  sge0resplit  46377  sge0split  46380  sge0splitmpt  46382  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0fodjrnlem  46387  sge0iunmpt  46389  sge0rpcpnf  46392  sge0ltfirpmpt2  46397  sge0isum  46398  sge0xaddlem1  46404  sge0xaddlem2  46405  sge0pnffsumgt  46413  sge0gtfsumgt  46414  sge0seq  46417  sge0reuz  46418  nnfoctbdjlem  46426  nnfoctbdj  46427  meadjun  46433  meadjiunlem  46436  voliunsge0lem  46443  meaiuninc3v  46455  omeiunltfirp  46490  carageniuncllem2  46493  caratheodorylem1  46497  caratheodorylem2  46498  caratheodory  46499  isomenndlem  46501  isomennd  46502  hoicvr  46519  volicorescl  46524  ovnsubaddlem2  46542  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvle  46571  ovnhoilem2  46573  hspdifhsp  46587  hoiqssbllem2  46594  hoiqssbllem3  46595  hspmbllem2  46598  ovnsubadd2lem  46616  ovolval4lem1  46620  vonvolmbl  46632  vonioo  46653  vonicc  46656  pimrecltpos  46679  issmfle  46716  smflimlem1  46742  smflimlem2  46743  smflimlem6  46747  smfresal  46759  smfrec  46760  smfmullem4  46765  smfpimcc  46779  smflimmpt  46781  smfsuplem1  46782  smfsuplem3  46784  smfsupmpt  46786  smfsupxr  46787  smfinflem  46788  smfinfmpt  46790  smflimsuplem4  46794  smflimsuplem5  46795  smflimsupmpt  46800  smfliminfmpt  46803  fsupdm  46813  finfdm  46817  smonoord  47345  lswn0  47418  poprelb  47498  fmtnoprmfac1  47539  fmtnofac2lem  47542  sbgoldbst  47752  isgrim  47855  gpgedgvtx0  48025  snlindsntorlem  48432  1arymaptf  48603  ipolubdm  48948  ipoglbdm  48951  setc1onsubc  49564  aacllem  49763