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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad2antlr  725  ad2ant2l  744  ad2ant2lr  746  ad5ant23  758  ad5ant24  759  ad5ant25  760  3adant1  1126  3ad2antl3  1183  ralcom2  3363  vtocl2d  3557  sbc2iegf  3849  sbcralt  3855  pofun  5491  poinxp  5632  xpdifid  6025  sossfld  6043  predpo  6166  preddowncl  6175  tz7.7  6217  onfr  6230  ssimaex  6748  fndmdif  6812  dffo4  6869  fcompt  6895  fconst2g  6965  f1cofveqaeq  7016  2f1fvneq  7018  isores3  7088  fvmptopab  7209  limsssuc  7565  el2mpocl  7781  1stconst  7795  2ndconst  7796  curry1  7799  curry2  7802  extmptsuppeq  7854  suppss  7860  suppssov1  7862  suppss2  7864  onnseq  7981  oe0  8147  oesuclem  8150  oecl  8162  oaordi  8172  oawordri  8176  omordi  8192  omword2  8200  omlimcl  8204  odi  8205  omass  8206  oeoe  8225  nnaordi  8244  oaabs  8271  omsmolem  8280  eceqoveq  8402  mapsnd  8450  dom2lem  8549  sbthlem9  8635  php3  8703  onomeneq  8708  isinf  8731  frfi  8763  fiint  8795  fodomfib  8798  fofinf1o  8799  marypha1lem  8897  ordiso2  8979  unwdomg  9048  xpwdomg  9049  ac5num  9462  cff1  9680  cfcoflem  9694  infpssrlem4  9728  isf32lem9  9783  isf34lem7  9801  fin1a2lem13  9834  fin1a2s  9836  hsmexlem4  9851  axdc2lem  9870  zorn2lem6  9923  axpowndlem2  10020  inttsk  10196  tskuni  10205  nqereu  10351  prcdnq  10415  addclprlem2  10439  ltexpri  10465  prlem936  10469  reclem2pr  10470  axsup  10716  add4  10860  ltleadd  11123  lt2mul2div  11518  nn2ge  11665  zextle  12056  fnn0ind  12082  xrlttr  12534  ifle  12591  xnn0lem1lt  12638  xaddass  12643  xmulasslem3  12680  xlemul1a  12682  xadddilem  12688  xrsupsslem  12701  xrinfmsslem  12702  supxrunb1  12713  supxrunb2  12714  ixxin  12756  difreicc  12871  iccsplit  12872  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  fzaddel  12942  fzadd2  12943  fzrev  12971  modadd1  13277  modmul1  13293  fsuppmapnn0fiub  13360  mulexp  13469  expadd  13472  expmul  13475  expnbnd  13594  bccl  13683  hashdom  13741  prsshashgt1  13772  hashfacen  13813  brfi1uzind  13857  wrdnval  13896  swrdccat3blem  14101  revccat  14128  2shfti  14439  rexico  14713  cau3lem  14714  subcn2  14951  caucvgb  15036  iseraltlem1  15038  sumss  15081  fsumsplitsn  15100  incexclem  15191  supcvg  15211  mertenslem2  15241  fprodn0  15333  fprodsplitsn  15343  fprodle  15350  eftlcl  15460  reeftlcl  15461  rpnnen2lem6  15572  dvdsext  15671  3dvds  15680  sqoddm1div8z  15703  gcdcllem3  15850  bezoutr1  15913  seq1st  15915  dvdslcm  15942  lcmeq0  15944  lcmcl  15945  lcmneg  15947  lcmdvds  15952  coprmgcdb  15993  dvdsprime  16031  pc2dvds  16215  prmpwdvds  16240  unbenlem  16244  infpnlem1  16246  1arith  16263  vdwmc2  16315  ramcl  16365  mrcuni  16892  isacs1i  16928  acsfn  16930  funcpropd  17170  curfcl  17482  curf2ndf  17497  resmhm  17985  resmhm2b  17987  mhmco  17988  mhmima  17989  pwsdiagmhm  17995  gsumwsubmcl  18001  gsumwspan  18011  pwmnd  18102  dfgrp2  18128  subgint  18303  ghmmhmb  18369  resghm  18374  cntzmhm  18469  symgextf1lem  18548  f1omvdconj  18574  dfod2  18691  gexdvds  18709  subgpgp  18722  sylow1lem3  18725  frgpnabllem1  18993  dprdfeq0  19144  isdrng2  19512  cntzsubr  19568  islmodd  19640  lsslss  19733  reslmhm2b  19826  psrbaglefi  20152  mptcoe1fsupp  20383  ply1coe  20464  psgnfix1  20742  psgndif  20746  copsgndif  20747  ocvocv  20815  frlmsslsp  20940  frlmlbs  20941  mamudi  21012  mamudir  21013  mat1dimelbas  21080  scmatmulcl  21127  scmatfo  21139  mulmarep1gsum2  21183  mdetunilem7  21227  mdetunilem9  21229  gsummatr01lem3  21266  smadiadetlem3  21277  cpmadugsumlemF  21484  leordtval  21821  cnpnei  21872  cnco  21874  cnss1  21884  cmpsub  22008  hauscmplem  22014  dissnlocfin  22137  ptbasid  22183  tx2cn  22218  upxp  22231  txindis  22242  xkoptsub  22262  xkopt  22263  trfbas2  22451  filconn  22491  trfil2  22495  filssufilg  22519  ufileu  22527  fixufil  22530  ufilen  22538  rnelfmlem  22560  flimclsi  22586  hauspwpwf1  22595  fclsopn  22622  fclsfnflim  22635  fclscmpi  22637  alexsubALTlem4  22658  ptcmplem5  22664  tgpmulg  22701  subgtgp  22713  tgpt0  22727  tsmsxplem2  22762  metss  23118  metustfbas  23167  dscopn  23183  xrsmopn  23420  cncfss  23507  icoopnst  23543  iccpnfcnv  23548  icccvx  23554  evth  23563  phtpycc  23595  pcohtpylem  23623  lmmbrf  23865  fgcfil  23874  caucfil  23886  cfilres  23899  bcth3  23934  cmscsscms  23976  ovolfioo  24068  ovolficc  24069  voliunlem3  24153  volcn  24207  mbflimsup  24267  mbfi1fseqlem5  24320  itg2seq  24343  dvnff  24520  dvnadd  24526  cpnord  24532  c1liplem1  24593  plypf1  24802  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  dgrle  24833  dgrnznn  24837  plycjlem  24866  elqaalem3  24910  ulmcaulem  24982  ulmcau  24983  psergf  25000  psercn2  25011  efopn  25241  abscxpbnd  25334  leibpi  25520  isppw2  25692  muinv  25770  bposlem3  25862  gausslemma2dlem4  25945  pntrmax  26140  pntpbnd1  26162  qabvexp  26202  eqeelen  26690  colinearalglem4  26695  axcgrid  26702  axsegconlem1  26703  axsegconlem3  26705  ax5seglem1  26714  ax5seglem2  26715  ax5seglem9  26723  axcontlem2  26751  cusgrfilem2  27238  vtxdgfisf  27258  usgr2pthlem  27544  uspgrn2crct  27586  crctcshwlkn0  27599  wwlksnext  27671  wwlksnextproplem3  27690  eupth2lem3lem4  28010  frgr3vlem1  28052  frgr3vlem2  28053  3vfriswmgrlem  28056  frgrwopreglem5  28100  numclwwlk3lem2  28163  grpoidinvlem3  28283  grpoidinv  28285  grpoideu  28286  nmoub3i  28550  nmlno0lem  28570  nmlnoubi  28573  ipasslem3  28610  ipblnfi  28632  hvaddsub4  28855  his35  28865  shsel3  29092  chj4  29312  spansncol  29345  chscllem2  29415  5oalem2  29432  3oalem2  29440  hoaddcl  29535  adjsym  29610  cnvadj  29669  hhcno  29681  hhcnf  29682  nmopub2tALT  29686  unoplin  29697  counop  29698  nmfnleub2  29703  hmoplin  29719  brafnmul  29728  nmlnop0iALT  29772  nmopun  29791  nmophmi  29808  riesz3i  29839  riesz1  29842  cnlnadjlem2  29845  cnlnadjlem6  29849  adjmul  29869  adjadd  29870  bra11  29885  cnvbraval  29887  kbass5  29897  kbass6  29898  leop2  29901  leopadd  29909  leopmuli  29910  leoptri  29913  leopnmid  29915  nmopleid  29916  pj3si  29984  hstel2  29996  cvcon3  30061  dmdmd  30077  dmdbr5  30085  mdsl0  30087  mdslmd1lem1  30102  mdslmd1lem2  30103  mdslmd3i  30109  superpos  30131  chirredlem2  30168  chirredlem3  30169  mdsymlem3  30182  mdsymlem5  30184  mdsymlem6  30185  sumdmdlem  30195  cdjreui  30209  cdj1i  30210  cdj3i  30218  foresf1o  30265  abfmpel  30400  fcomptf  30403  fcnvgreu  30418  xrge0infss  30484  xnn0gt0  30494  cycpm2tr  30761  lssdimle  31006  mdetpmtr1  31088  cmpcref  31114  xrge0iifcnv  31176  esumcst  31322  hasheuni  31344  esum2dlem  31351  esum2d  31352  sigaclcu2  31379  insiga  31396  unelldsys  31417  measres  31481  measdivcst  31483  volfiniune  31489  ddemeas  31495  sgn3da  31799  actfunsnf1o  31875  sconnpi1  32486  cvmsss2  32521  satfv1lem  32609  fmlaomn0  32637  gonarlem  32641  mrsubco  32768  dfon2lem6  33033  dftrpred3g  33072  poseq  33095  soseq  33096  frr1  33144  hfext  33644  elicc3  33665  fnessref  33705  bj-ismooredr2  34405  pibt2  34701  fin2solem  34893  fin2so  34894  lindsenlbs  34902  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem2  34909  poimirlem14  34921  poimirlem25  34932  poimirlem26  34933  poimirlem29  34936  poimirlem30  34937  broucube  34941  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ex-ovoliunnfl  34950  mbfresfi  34953  cnambfre  34955  itg2addnclem  34958  itg2addnclem2  34959  itg2addnc  34961  bddiblnc  34977  ftc1anclem3  34984  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  eqfnun  35012  indexdom  35024  filbcmb  35030  fdc  35035  incsequz  35038  metf1o  35045  caures  35050  bndss  35079  ismtycnv  35095  heiborlem1  35104  rrncmslem  35125  isdrngo2  35251  rngoisocnv  35274  unichnidl  35324  erim2  35926  ax12eq  36092  ax12el  36093  lshpset2N  36270  pmapglb2N  36922  pmapglb2xN  36923  pclfinN  37051  polval2N  37057  cdleme31fv2  37544  cdleme32fvcl  37591  cdleme48gfv  37688  tendoicl  37947  tendoipl  37948  diaglbN  38206  dochkr1  38629  dochkr1OLDN  38630  selvval2lem5  39186  dvdsexpim  39230  nacsfix  39358  eq0rabdioph  39422  diophren  39459  rencldnfilem  39466  pell1234qrdich  39507  jm2.24  39609  jm2.26lem3  39647  wepwsolem  39691  pwssplit4  39738  isnumbasgrplem3  39754  grumnudlem  40670  cvgdvgrat  40694  ofsubid  40705  bcc0  40721  binomcxplemnn0  40730  uzwo4  41364  fiiuncl  41376  iunincfi  41409  nsstr  41410  rexanuz3  41411  iinssiin  41444  ralimda  41455  disjrnmpt2  41498  fompt  41502  disjinfi  41503  choicefi  41512  fsneq  41518  difmap  41519  iunmapsn  41529  axccdom  41536  axccd  41544  rnmptlb  41563  rnmptbd2lem  41569  ssfiunibd  41625  supxrgelem  41654  suplesup  41656  xrlexaddrp  41669  xralrple2  41671  infxrunb2  41685  xralrple3  41691  xrralrecnnle  41702  xrralrecnnge  41711  supxrunb3  41721  unb2ltle  41738  rexabslelem  41741  supminfrnmpt  41768  infxrpnf  41770  supminfxr  41789  supminfxr2  41794  xrpnf  41811  iooiinicc  41867  ressioosup  41880  iooiinioc  41881  ressiooinf  41882  fsumsupp0  41908  divcnvg  41957  limcrecl  41959  sumnnodd  41960  islpcn  41969  lptre2pt  41970  limcresiooub  41972  limcresioolb  41973  limclner  41981  fnlimfvre  42004  allbutfifvre  42005  climinf3  42046  limsupmnflem  42050  limsupre3uzlem  42065  limsupreuzmpt  42069  climuzlem  42073  climisp  42076  climrescn  42078  climxrrelem  42079  climxrre  42080  climlimsupcex  42099  liminflelimsuplem  42105  limsupgtlem  42107  liminfvalxr  42113  liminfreuzlem  42132  liminfltlem  42134  liminflimsupclim  42137  xlimpnfxnegmnf  42144  liminflbuz2  42145  liminflimsupxrre  42147  cnrefiisplem  42159  xlimmnfvlem2  42163  xlimmnfv  42164  xlimpnfvlem2  42167  xlimpnfv  42168  xlimmnfmpt  42173  xlimpnfmpt  42174  climxlim2lem  42175  dfxlim2v  42177  xlimliminflimsup  42192  cncfuni  42218  icccncfext  42219  cncficcgt0  42220  cncfiooicclem1  42225  cncfiooiccre  42227  dvasinbx  42254  dvdsn1add  42273  dvnmul  42277  dvmptfprodlem  42278  dvnprodlem1  42280  dvnprodlem3  42282  iblspltprt  42307  itgioocnicc  42311  itgspltprt  42313  ismbl3  42320  stirlinglem5  42412  dirker2re  42426  dirkerper  42430  dirkertrigeq  42435  dirkercncflem2  42438  fourierdlem12  42453  fourierdlem15  42456  fourierdlem16  42457  fourierdlem20  42461  fourierdlem21  42462  fourierdlem22  42463  fourierdlem39  42480  fourierdlem40  42481  fourierdlem41  42482  fourierdlem42  42483  fourierdlem46  42486  fourierdlem49  42489  fourierdlem50  42490  fourierdlem57  42497  fourierdlem58  42498  fourierdlem59  42499  fourierdlem64  42504  fourierdlem65  42505  fourierdlem66  42506  fourierdlem68  42508  fourierdlem70  42510  fourierdlem71  42511  fourierdlem73  42513  fourierdlem78  42518  fourierdlem79  42519  fourierdlem80  42520  fourierdlem81  42521  fourierdlem82  42522  fourierdlem83  42523  fourierdlem87  42527  fourierdlem93  42533  fourierdlem95  42535  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  sqwvfoura  42562  fourierswlem  42564  elaa2lem  42567  etransclem13  42581  etransclem23  42591  etransclem24  42592  etransclem32  42600  etransclem38  42606  etransclem46  42614  qndenserrnbllem  42628  rrxsnicc  42634  ioorrnopnlem  42638  prsal  42652  intsal  42662  salexct  42666  dfsalgen2  42673  issalnnd  42677  sge0rnre  42695  sge0val  42697  sge0z  42706  sge0revalmpt  42709  sge0tsms  42711  sge0pr  42725  sge0resplit  42737  sge0split  42740  sge0splitmpt  42742  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  sge0fodjrnlem  42747  sge0iunmpt  42749  sge0rpcpnf  42752  sge0ltfirpmpt2  42757  sge0isum  42758  sge0xaddlem1  42764  sge0xaddlem2  42765  sge0pnffsumgt  42773  sge0gtfsumgt  42774  sge0seq  42777  sge0reuz  42778  nnfoctbdjlem  42786  nnfoctbdj  42787  meadjun  42793  meadjiunlem  42796  voliunsge0lem  42803  meaiuninc3v  42815  omeiunltfirp  42850  carageniuncllem2  42853  caratheodorylem1  42857  caratheodorylem2  42858  caratheodory  42859  isomenndlem  42861  isomennd  42862  hoicvr  42879  volicorescl  42884  ovnsubaddlem2  42902  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvle  42931  ovnhoilem2  42933  hspdifhsp  42947  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem2  42958  ovnsubadd2lem  42976  ovolval4lem1  42980  vonvolmbl  42992  vonioo  43013  vonicc  43016  pimrecltpos  43036  issmfle  43071  smflimlem1  43096  smflimlem2  43097  smflimlem6  43101  smfresal  43112  smfrec  43113  smfmullem4  43118  smfpimcc  43131  smflimmpt  43133  smfsuplem1  43134  smfsuplem3  43136  smfsupmpt  43138  smfsupxr  43139  smfinflem  43140  smfinfmpt  43142  smflimsuplem4  43146  smflimsuplem5  43147  smflimsupmpt  43152  smfliminfmpt  43155  smonoord  43580  lswn0  43653  poprelb  43735  fmtnoprmfac1  43776  fmtnofac2lem  43779  sbgoldbst  43992  resmgmhm  44114  resmgmhm2b  44116  mgmhmco  44117  mgmhmima  44118  snlindsntorlem  44574  aacllem  44951