Theorem adantll 727

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad2antlr  740  ad2ant2l  759  ad2ant2lr  761  ad5ant23  772  ad5ant24  773  ad5ant25  774  3adant1  1148  3ad2antl3  1206  ralcom2  3368  vtocl2d  3530  sbc2iegf  3820  sbcralt  3826  pofun  5589  poinxp  5744  xpdifid  6167  xpdifcnvepel  6168  sossfld  6186  preddowncl  6337  tz7.7  6390  onfr  6404  ssimaex  6970  fsneq  7034  eqfnun  7036  fndmdif  7041  dffo4  7102  fompt  7117  fcompt  7133  fconst2g  7205  f1cofveqaeq  7257  isores3  7339  limsssuc  7848  el2mpocl  8083  1stconst  8097  2ndconst  8098  curry1  8101  curry2  8104  poseq  8156  soseq  8157  extmptsuppeq  8186  suppss  8192  suppss2  8198  onnseq  8333  oe0  8509  oesuclem  8512  oecl  8524  oaordi  8533  oawordri  8537  omordi  8553  omword2  8561  omlimcl  8565  odi  8566  omass  8567  oeoe  8587  nnaordi  8606  oaabs  8636  omsmolem  8645  eceqoveq  8822  mapsnd  8886  dom2lem  8991  sbthlem9  9086  rexdif1en  9148  isinf  9228  frfi  9248  fiint  9289  fodomfib  9291  fofinf1o  9292  marypha1lem  9396  ordiso2  9480  unwdomg  9549  xpwdomg  9550  frr1  9734  ac5num  10032  cff1  10253  cfcoflem  10267  infpssrlem4  10301  isf32lem9  10356  isf34lem7  10374  fin1a2lem13  10407  fin1a2s  10409  hsmexlem4  10424  axdc2lem  10443  zorn2lem6  10496  axpowndlem2  10594  inttsk  10770  tskuni  10779  nqereu  10925  prcdnq  10989  addclprlem2  11013  ltexpri  11039  prlem936  11043  reclem2pr  11044  axsup  11296  add4  11442  ltleadd  11708  lt2mul2div  12104  nn2ge  12274  zextle  12681  fnn0ind  12707  xrlttr  13177  ifle  13235  xnn0lem1lt  13282  xaddass  13287  xmulasslem3  13324  xlemul1a  13326  xadddilem  13332  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  supxrunb2  13358  ixxin  13401  difreicc  13523  iccsplit  13524  iccshftr  13525  iccshftl  13527  iccdil  13529  icccntr  13531  fzaddel  13599  fzadd2  13600  fzrev  13628  modadd1  13955  modmul1  13974  fsuppmapnn0fiub  14041  mulexp  14151  expadd  14154  expmul  14157  expnbnd  14282  bccl  14372  hashdom  14429  prsshashgt1  14461  hashfacen  14505  brfi1uzind  14559  wrdnval  14596  swrdccat3blem  14794  revccat  14821  2shfti  15137  sgn3da  15158  rexico  15425  cau3lem  15426  subcn2  15666  caucvgb  15751  iseraltlem1  15753  sumss  15794  fsumsplitsn  15814  incexclem  15909  supcvg  15929  mertenslem2  15958  fprodn0  16052  fprodsplitsn  16062  fprodle  16069  eftlcl  16181  reeftlcl  16182  rpnnen2lem6  16293  dvdsext  16397  3dvds  16407  sqoddm1div8z  16430  gcdcllem3  16577  dvdsexpim  16631  bezoutr1  16645  seq1st  16647  dvdslcm  16674  lcmeq0  16676  lcmcl  16677  lcmneg  16679  lcmdvds  16684  coprmgcdb  16725  dvdsprime  16763  pc2dvds  16957  prmpwdvds  16982  unbenlem  16986  infpnlem1  16988  1arith  17005  vdwmc2  17057  ramcl  17107  mrcuni  17695  isacs1i  17731  acsfn  17733  funcpropd  17977  curfcl  18306  curf2ndf  18321  resmgmhm  18791  resmgmhm2b  18793  mgmhmco  18794  mgmhmima  18795  resmhm  18903  resmhm2b  18905  mhmco  18906  pwsdiagmhm  18914  gsumwsubmcl  18920  gsumwspan  18929  pwmnd  19023  dfgrp2  19053  subgint  19241  ghmmhmb  19321  resghm  19326  cntzmhm  19435  symgextf1lem  19514  f1omvdconj  19540  dfod2  19658  gexdvds  19678  subgpgp  19691  sylow1lem3  19694  frgpnabllem1  19967  dprdfeq0  20118  rhmimasubrnglem  20694  cntzsubrng  20696  cntzsubr  20735  isdrng2  20873  isdrng3lem1  20881  islmodd  21017  lsslss  21112  reslmhm2b  21205  rngqiprngimfo  21471  rhmpreimaprmidl  21509  psgnfix1  21778  psgndif  21782  copsgndif  21783  ocvocv  21851  frlmsslsp  21976  frlmlbs  21977  psrbaglefi  22106  psrdi  22144  psrass23l  22146  psrass23  22148  evlsvvval  22274  rhmcomulmpl  22305  selvcllem5  22320  psdmul  22359  mptcoe1fsupp  22405  psropprmul  22427  ply1coe  22488  mamudi  22590  mamudir  22591  mat1dimelbas  22658  scmatmulcl  22705  scmatfo  22717  mulmarep1gsum2  22761  mdetunilem7  22805  mdetunilem9  22807  gsummatr01lem3  22844  smadiadetlem3  22855  cpmadugsumlemF  23063  leordtval  23400  cnpnei  23451  cnco  23453  cnss1  23463  cmpsub  23587  hauscmplem  23593  dissnlocfin  23717  ptbasid  23763  tx2cn  23798  upxp  23811  txindis  23822  xkoptsub  23842  xkopt  23843  trfbas2  24031  filconn  24071  trfil2  24075  filssufilg  24099  ufileu  24107  fixufil  24110  ufilen  24118  rnelfmlem  24140  flimclsi  24166  hauspwpwf1  24175  fclsopn  24202  fclsfnflim  24215  fclscmpi  24217  alexsubALTlem4  24238  ptcmplem5  24244  tgpmulg  24281  subgtgp  24293  tgpt0  24307  tsmsxplem2  24342  metss  24696  metustfbas  24745  dscopn  24761  xrsmopn  25001  cncfss  25089  icoopnst  25129  iccpnfcnv  25134  icccvx  25140  evth  25149  phtpycc  25181  pcohtpylem  25209  lmmbrf  25452  fgcfil  25461  caucfil  25473  cfilres  25486  bcth3  25521  cmscsscms  25563  ovolfioo  25657  ovolficc  25658  voliunlem3  25742  volcn  25796  mbflimsup  25856  mbfi1fseqlem5  25909  itg2seq  25932  bddiblnc  26032  dvnff  26113  dvnadd  26119  cpnord  26125  c1liplem1  26186  plypf1  26400  plyaddlem1  26401  plymullem1  26402  coeeulem  26412  coeidlem  26425  dgrle  26431  dgrnznn  26435  plycjlem  26464  elqaalem3  26513  ulmcaulem  26588  ulmcau  26589  psergf  26606  psercn2  26617  efopn  26854  abscxpbnd  26949  leibpi  27138  isppw2  27310  muinv  27388  bposlem3  27481  gausslemma2dlem4  27564  pntrmax  27759  pntpbnd1  27781  qabvexp  27821  madebday  28124  mulsrid  28337  bdayons  28500  peano5n0s  28543  bdaypw2n0bndlem  28687  bdayfinlem  28710  eqeelen  29285  colinearalglem4  29290  axcgrid  29297  axsegconlem1  29298  axsegconlem3  29300  ax5seglem1  29309  ax5seglem2  29310  ax5seglem9  29318  axcontlem2  29346  cusgrfilem2  29840  vtxdgfisf  29860  usgr2pthlem  30152  uspgrn2crct  30200  crctcshwlkn0  30213  wwlksnext  30285  wwlksnextproplem3  30303  eupth2lem3lem4  30629  frgr3vlem1  30671  frgr3vlem2  30672  3vfriswmgrlem  30675  frgrwopreglem5  30719  numclwwlk3lem2  30782  grpoidinvlem3  30905  grpoidinv  30907  grpoideu  30908  nmoub3i  31172  nmlno0lem  31192  nmlnoubi  31195  ipasslem3  31232  ipblnfi  31254  hvaddsub4  31477  his35  31487  shsel3  31714  chj4  31934  spansncol  31967  chscllem2  32037  5oalem2  32054  3oalem2  32062  hoaddcl  32157  adjsym  32232  cnvadj  32291  hhcno  32303  hhcnf  32304  nmopub2tALT  32308  unoplin  32319  counop  32320  nmfnleub2  32325  hmoplin  32341  brafnmul  32350  nmlnop0iALT  32394  nmopun  32413  nmophmi  32430  riesz3i  32461  riesz1  32464  cnlnadjlem2  32467  cnlnadjlem6  32471  adjmul  32491  adjadd  32492  bra11  32507  cnvbraval  32509  kbass5  32519  kbass6  32520  leop2  32523  leopadd  32531  leopmuli  32532  leoptri  32535  leopnmid  32537  nmopleid  32538  pj3si  32606  hstel2  32618  cvcon3  32683  dmdmd  32699  dmdbr5  32707  mdsl0  32709  mdslmd1lem1  32724  mdslmd1lem2  32725  mdslmd3i  32731  superpos  32753  chirredlem2  32790  chirredlem3  32791  mdsymlem3  32804  mdsymlem5  32806  mdsymlem6  32807  sumdmdlem  32817  cdjreui  32831  cdj1i  32832  cdj3i  32840  foresf1o  32897  2ndimaxp  33038  abfmpel  33047  fcomptf  33050  fcnvgreu  33064  fdifsuppconst  33081  xrge0infss  33151  xnn0gt0  33160  cycpm2tr  33479  elrgspnlem2  33603  elrgspnlem3  33604  intlidl  33768  mplvrpmga  33975  psrmonmul  33980  esplyfval0  33994  vieta  34010  lssdimle  34038  mdetpmtr1  34253  cmpcref  34280  xrge0iifcnv  34363  zrhcntr  34409  esumcst  34493  hasheuni  34515  esum2dlem  34522  esum2d  34523  sigaclcu2  34550  insiga  34568  unelldsys  34589  measres  34653  measdivcst  34655  volfiniune  34661  ddemeas  34667  actfunsnf1o  35032  fnrelpredd  35516  fineqvac  35562  fineqvnttrclselem1  35567  sconnpi1  35744  cvmsss2  35779  satfv1lem  35867  fmlaomn0  35895  gonarlem  35899  mrsubco  36026  dfon2lem6  36291  hfext  36688  elicc3  36861  fnessref  36901  bj-ismooredr2  37785  pibt2  38096  fin2solem  38290  fin2so  38291  lindsenlbs  38299  matunitlindflem1  38300  matunitlindflem2  38301  poimirlem2  38306  poimirlem14  38318  poimirlem25  38329  poimirlem26  38330  poimirlem29  38333  poimirlem30  38334  broucube  38338  heicant  38339  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  ex-ovoliunnfl  38347  mbfresfi  38350  cnambfre  38352  itg2addnclem  38355  itg2addnclem2  38356  itg2addnc  38358  ftc1anclem3  38379  ftc1anclem4  38380  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  indexdom  38418  filbcmb  38424  fdc  38429  incsequz  38432  metf1o  38439  caures  38444  bndss  38470  ismtycnv  38486  heiborlem1  38495  rrncmslem  38516  isdrngo2  38642  rngoisocnv  38665  unichnidl  38715  erimeq2  39445  ax12eq  39748  ax12el  39749  lshpset2N  39926  pmapglb2N  40578  pmapglb2xN  40579  pclfinN  40707  polval2N  40713  cdleme31fv2  41200  cdleme32fvcl  41247  cdleme48gfv  41344  tendoicl  41603  tendoipl  41604  diaglbN  41862  dochkr1  42285  dochkr1OLDN  42286  sumcubes  43107  expeq1d  43118  zaddcomlem  43270  zmulcomlem  43274  fiabv  43337  rhmcomulpsr  43347  evlselv  43354  fsuppind  43355  fsuppssind  43358  mhpind  43359  nacsfix  43476  eq0rabdioph  43540  diophren  43573  rencldnfilem  43580  pell1234qrdich  43621  jm2.24  43723  jm2.26lem3  43761  wepwsolem  43802  pwssplit4  43849  isnumbasgrplem3  43865  onexoegt  44004  onov0suclim  44034  cantnfresb  44084  omcl2  44093  ofoaid1  44118  ofoaid2  44119  grumnudlem  45028  cvgdvgrat  45056  ofsubid  45067  bcc0  45083  binomcxplemnn0  45092  uzwo4  45806  fiiuncl  45818  iunincfi  45845  nsstr  45846  rexanuz3  45847  iinssiin  45880  disjrnmpt2  45939  disjinfi  45943  choicefi  45950  difmap  45956  iunmapsn  45966  axccdom  45971  axccd  45977  rnmptlb  45991  rnmptbd2lem  45996  ssfiunibd  46061  supxrgelem  46086  suplesup  46088  xrlexaddrp  46101  xralrple2  46103  infxrunb2  46116  xralrple3  46122  xrralrecnnle  46131  xrralrecnnge  46138  supxrunb3  46147  unb2ltle  46162  rexabslelem  46165  supminfrnmpt  46192  infxrpnf  46193  supminfxr  46211  supminfxr2  46216  xrpnf  46232  pimxrneun  46235  cvgcaule  46238  iooiinicc  46291  ressioosup  46304  iooiinioc  46305  ressiooinf  46306  fsumsupp0  46327  divcnvg  46376  limcrecl  46378  sumnnodd  46379  islpcn  46386  lptre2pt  46387  limcresiooub  46389  limcresioolb  46390  limclner  46398  fnlimfvre  46421  allbutfifvre  46422  climinf3  46463  limsupmnflem  46467  limsupre3uzlem  46482  limsupreuzmpt  46486  climuzlem  46490  climisp  46493  climrescn  46495  climxrrelem  46496  climxrre  46497  climlimsupcex  46516  liminflelimsuplem  46522  limsupgtlem  46524  liminfvalxr  46530  liminfreuzlem  46549  liminfltlem  46551  liminflimsupclim  46554  xlimpnfxnegmnf  46561  liminflbuz2  46562  liminflimsupxrre  46564  cnrefiisplem  46576  xlimmnfvlem2  46580  xlimmnfv  46581  xlimpnfvlem2  46584  xlimpnfv  46585  xlimmnfmpt  46590  xlimpnfmpt  46591  climxlim2lem  46592  dfxlim2v  46594  xlimliminflimsup  46609  cncfuni  46633  icccncfext  46634  cncficcgt0  46635  cncfiooicclem1  46640  cncfiooiccre  46642  dvasinbx  46667  dvdsn1add  46686  dvnmul  46690  dvmptfprodlem  46691  dvnprodlem1  46693  dvnprodlem3  46695  iblspltprt  46720  itgioocnicc  46724  itgspltprt  46726  ismbl3  46733  stirlinglem5  46825  dirker2re  46839  dirkerper  46843  dirkertrigeq  46848  dirkercncflem2  46851  fourierdlem12  46866  fourierdlem15  46869  fourierdlem16  46870  fourierdlem20  46874  fourierdlem21  46875  fourierdlem22  46876  fourierdlem39  46893  fourierdlem40  46894  fourierdlem41  46895  fourierdlem42  46896  fourierdlem46  46899  fourierdlem49  46902  fourierdlem50  46903  fourierdlem57  46910  fourierdlem58  46911  fourierdlem59  46912  fourierdlem64  46917  fourierdlem65  46918  fourierdlem66  46919  fourierdlem68  46921  fourierdlem70  46923  fourierdlem71  46924  fourierdlem73  46926  fourierdlem78  46931  fourierdlem79  46932  fourierdlem80  46933  fourierdlem81  46934  fourierdlem82  46935  fourierdlem83  46936  fourierdlem87  46940  fourierdlem93  46946  fourierdlem95  46948  fourierdlem101  46954  fourierdlem103  46956  fourierdlem104  46957  fourierdlem111  46964  fourierdlem112  46965  sqwvfoura  46975  fourierswlem  46977  elaa2lem  46980  etransclem13  46994  etransclem23  47004  etransclem24  47005  etransclem32  47013  etransclem38  47019  etransclem46  47027  qndenserrnbllem  47041  rrxsnicc  47047  ioorrnopnlem  47051  prsal  47065  intsal  47077  salexct  47081  dfsalgen2  47088  issalnnd  47092  sge0rnre  47111  sge0val  47113  sge0z  47122  sge0revalmpt  47125  sge0tsms  47127  sge0pr  47141  sge0resplit  47153  sge0split  47156  sge0splitmpt  47158  sge0iunmptlemfi  47160  sge0iunmptlemre  47162  sge0fodjrnlem  47163  sge0iunmpt  47165  sge0rpcpnf  47168  sge0ltfirpmpt2  47173  sge0isum  47174  sge0xaddlem1  47180  sge0xaddlem2  47181  sge0pnffsumgt  47189  sge0gtfsumgt  47190  sge0seq  47193  sge0reuz  47194  nnfoctbdjlem  47202  nnfoctbdj  47203  meadjun  47209  meadjiunlem  47212  voliunsge0lem  47219  meaiuninc3v  47231  omeiunltfirp  47266  carageniuncllem2  47269  caratheodorylem1  47273  caratheodorylem2  47274  caratheodory  47275  isomenndlem  47277  isomennd  47278  hoicvr  47295  volicorescl  47300  ovnsubaddlem2  47318  hoidmvlelem2  47343  hoidmvlelem3  47344  hoidmvle  47347  ovnhoilem2  47349  hspdifhsp  47363  hoiqssbllem2  47370  hoiqssbllem3  47371  hspmbllem2  47374  ovnsubadd2lem  47392  ovolval4lem1  47396  vonvolmbl  47408  vonioo  47429  vonicc  47432  pimrecltpos  47455  issmfle  47492  smflimlem1  47518  smflimlem2  47519  smflimlem6  47523  smfresal  47535  smfrec  47536  smfmullem4  47541  smfpimcc  47555  smflimmpt  47557  smfsuplem1  47558  smfsuplem3  47560  smfsupmpt  47562  smfsupxr  47563  smfinflem  47564  smfinfmpt  47566  smflimsuplem4  47570  smflimsuplem5  47571  smflimsupmpt  47576  smfliminfmpt  47579  fsupdm  47589  finfdm  47593  smonoord  48147  lswn0  48226  poprelb  48306  fmtnoprmfac1  48350  fmtnofac2lem  48353  sbgoldbst  48576  isgrim  48680  gpgedgvtx0  48859  snlindsntorlem  49283  1arymaptf  49454  ipolubdm  49798  ipoglbdm  49801  setc1onsubc  50413  aacllem  50654