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  3362  vtocl2d  3523  sbc2iegf  3813  sbcralt  3819  pofun  5581  poinxp  5736  xpdifid  6160  xpdifcnvepel  6161  sossfld  6179  preddowncl  6330  tz7.7  6383  onfr  6397  ssimaex  6963  fsneq  7027  eqfnun  7029  fndmdif  7034  dffo4  7096  fompt  7111  fcompt  7127  fconst2g  7202  f1cofveqaeq  7254  isores3  7336  limsssuc  7846  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  8893  dom2lem  8998  sbthlem9  9093  rexdif1en  9155  isinf  9235  frfi  9255  fiint  9296  fodomfib  9298  fofinf1o  9299  marypha1lem  9403  ordiso2  9487  unwdomg  9556  xpwdomg  9557  frr1  9741  ac5num  10039  cff1  10260  cfcoflem  10274  infpssrlem4  10308  isf32lem9  10363  isf34lem7  10381  fin1a2lem13  10414  fin1a2s  10416  hsmexlem4  10431  axdc2lem  10450  zorn2lem6  10503  axpowndlem2  10607  inttsk  10783  tskuni  10792  nqereu  10938  prcdnq  11002  addclprlem2  11026  ltexpri  11052  prlem936  11056  reclem2pr  11057  axsup  11309  add4  11455  ltleadd  11721  lt2mul2div  12117  nn2ge  12287  zextle  12694  fnn0ind  12720  xrlttr  13191  ifle  13249  xnn0lem1lt  13296  xaddass  13301  xmulasslem3  13338  xlemul1a  13340  xadddilem  13346  xrsupsslem  13359  xrinfmsslem  13360  supxrunb1  13371  supxrunb2  13372  ixxin  13415  difreicc  13537  iccsplit  13538  iccshftr  13539  iccshftl  13541  iccdil  13543  icccntr  13545  fzaddel  13613  fzadd2  13614  fzrev  13642  modadd1  13969  modmul1  13988  fsuppmapnn0fiub  14055  mulexp  14165  expadd  14168  expmul  14171  expnbnd  14296  bccl  14386  hashdom  14443  prsshashgt1  14475  hashfacen  14519  brfi1uzind  14573  wrdnval  14610  swrdccat3blem  14808  revccat  14835  2shfti  15153  sgn3da  15174  rexico  15441  cau3lem  15442  subcn2  15682  caucvgb  15767  iseraltlem1  15769  sumss  15810  fsumsplitsn  15830  incexclem  15925  supcvg  15945  mertenslem2  15974  fprodn0  16066  fprodsplitsn  16076  fprodle  16083  eftlcl  16195  reeftlcl  16196  rpnnen2lem6  16307  dvdsext  16411  3dvds  16421  sqoddm1div8z  16444  gcdcllem3  16591  dvdsexpim  16645  bezoutr1  16659  seq1st  16661  dvdslcm  16688  lcmeq0  16690  lcmcl  16691  lcmneg  16693  lcmdvds  16698  coprmgcdb  16739  dvdsprime  16777  pc2dvds  16971  prmpwdvds  16996  unbenlem  17000  infpnlem1  17002  1arith  17019  vdwmc2  17071  ramcl  17121  mrcuni  17709  isacs1i  17745  acsfn  17747  funcpropd  17991  curfcl  18320  curf2ndf  18335  mgmidpfod  18770  resmgmhm  18813  resmgmhm2b  18815  mgmhmco  18816  mgmhmima  18817  resmhm  18929  resmhm2b  18931  mhmco  18932  pwsdiagmhm  18940  gsumwsubmcl  18946  gsumwspan  18955  pwmnd  19056  dfgrp2  19086  subgint  19274  ghmmhmb  19354  resghm  19359  cntzmhm  19468  symgextf1lem  19547  f1omvdconj  19573  dfod2  19691  gexdvds  19711  subgpgp  19724  sylow1lem3  19727  frgpnabllem1  20000  dprdfeq0  20151  rhmimasubrnglem  20727  cntzsubrng  20729  cntzsubr  20768  isdrng2  20906  isdrng3lem1  20914  islmodd  21050  lsslss  21145  reslmhm2b  21238  rngqiprngimfo  21504  rhmpreimaprmidl  21542  psgnfix1  21811  psgndif  21815  copsgndif  21816  ocvocv  21884  frlmsslsp  22009  frlmlbs  22010  lindsenlbs  22064  psrbaglefi  22141  psrdi  22179  psrass23l  22181  psrass23  22183  evlsvvval  22309  rhmcomulmpl  22340  selvcllem5  22355  psdmul  22394  mptcoe1fsupp  22440  psropprmul  22462  ply1coe  22523  mamudi  22625  mamudir  22626  mat1dimelbas  22693  scmatmulcl  22740  scmatfo  22752  mulmarep1gsum2  22796  mdetunilem7  22840  mdetunilem9  22842  gsummatr01lem3  22879  smadiadetlem3  22890  matunitlindflem1  22901  matunitlindflem2  22902  cpmadugsumlemF  23101  leordtval  23438  cnpnei  23489  cnco  23491  cnss1  23501  cmpsub  23625  hauscmplem  23631  dissnlocfin  23755  ptbasid  23801  tx2cn  23836  upxp  23849  txindis  23860  xkoptsub  23880  xkopt  23881  trfbas2  24069  filconn  24109  trfil2  24113  filssufilg  24137  ufileu  24145  fixufil  24148  ufilen  24156  rnelfmlem  24178  flimclsi  24204  hauspwpwf1  24213  fclsopn  24240  fclsfnflim  24253  fclscmpi  24255  alexsubALTlem4  24276  ptcmplem5  24282  tgpmulg  24319  subgtgp  24331  tgpt0  24345  tsmsxplem2  24380  metss  24734  metustfbas  24783  dscopn  24799  xrsmopn  25039  cncfss  25127  icoopnst  25167  iccpnfcnv  25172  icccvx  25178  evth  25187  phtpycc  25219  pcohtpylem  25247  lmmbrf  25490  fgcfil  25499  caucfil  25511  cfilres  25524  bcth3  25559  cmscsscms  25601  ovolfioo  25695  ovolficc  25696  voliunlem3  25780  volcn  25834  mbflimsup  25894  mbfi1fseqlem5  25947  itg2seq  25970  bddiblnc  26069  dvnff  26150  dvnadd  26156  cpnord  26162  c1liplem1  26223  plypf1  26438  plyaddlem1  26439  plymullem1  26440  coeeulem  26450  coeidlem  26463  dgrle  26469  dgrnznn  26473  plycjlem  26502  elqaalem3  26553  ulmcaulem  26630  ulmcau  26631  psergf  26648  psercn2  26659  efopn  26895  abscxpbnd  26990  leibpi  27179  isppw2  27351  muinv  27429  bposlem3  27522  gausslemma2dlem4  27605  pntrmax  27800  pntpbnd1  27822  qabvexp  27862  madebday  28165  mulsrid  28378  bdayons  28541  peano5n0s  28584  bdaypw2n0bndlem  28728  bdayfinlem  28751  eqeelen  29361  colinearalglem4  29366  axcgrid  29373  axsegconlem1  29374  axsegconlem3  29376  ax5seglem1  29385  ax5seglem2  29386  ax5seglem9  29394  axcontlem2  29422  cusgrfilem2  29916  vtxdgfisf  29936  usgr2pthlem  30228  uspgrn2crct  30276  crctcshwlkn0  30289  wwlksnext  30361  wwlksnextproplem3  30379  eupth2lem3lem4  30711  frgr3vlem1  30753  frgr3vlem2  30754  3vfriswmgrlem  30757  frgrwopreglem5  30801  numclwwlk3lem2  30864  grpoidinvlem3  30987  grpoidinv  30989  grpoideu  30990  nmoub3i  31254  nmlno0lem  31274  nmlnoubi  31277  ipasslem3  31314  ipblnfi  31336  hvaddsub4  31559  his35  31569  shsel3  31796  chj4  32016  spansncol  32049  chscllem2  32119  5oalem2  32136  3oalem2  32144  hoaddcl  32239  adjsym  32314  cnvadj  32373  hhcno  32385  hhcnf  32386  nmopub2tALT  32390  unoplin  32401  counop  32402  nmfnleub2  32407  hmoplin  32423  brafnmul  32432  nmlnop0iALT  32476  nmopun  32495  nmophmi  32512  riesz3i  32543  riesz1  32546  cnlnadjlem2  32549  cnlnadjlem6  32553  adjmul  32573  adjadd  32574  bra11  32589  cnvbraval  32591  kbass5  32601  kbass6  32602  leop2  32605  leopadd  32613  leopmuli  32614  leoptri  32617  leopnmid  32619  nmopleid  32620  pj3si  32688  hstel2  32700  cvcon3  32765  dmdmd  32781  dmdbr5  32789  mdsl0  32791  mdslmd1lem1  32806  mdslmd1lem2  32807  mdslmd3i  32813  superpos  32835  chirredlem2  32872  chirredlem3  32873  mdsymlem3  32886  mdsymlem5  32888  mdsymlem6  32889  sumdmdlem  32899  cdjreui  32913  cdj1i  32914  cdj3i  32922  foresf1o  32979  2ndimaxp  33119  abfmpel  33128  fcomptf  33131  fcnvgreu  33145  fdifsuppconst  33161  xrge0infss  33231  xnn0gt0  33240  cycpm2tr  33559  elrgspnlem2  33683  elrgspnlem3  33684  intlidl  33848  mplvrpmga  34055  psrmonmul  34060  esplyfval0  34074  vieta  34090  lssdimle  34118  mdetpmtr1  34333  cmpcref  34360  xrge0iifcnv  34443  zrhcntr  34489  esumcst  34573  hasheuni  34595  esum2dlem  34602  esum2d  34603  sigaclcu2  34630  insiga  34648  unelldsys  34669  measres  34733  measdivcst  34735  volfiniune  34741  ddemeas  34747  actfunsnf1o  35112  fnrelpredd  35596  fineqvac  35642  fineqvnttrclselem1  35647  sconnpi1  35818  cvmsss2  35853  satfv1lem  35941  fmlaomn0  35969  gonarlem  35973  mrsubco  36100  dfon2lem6  36365  hfext  36763  elicc3  36936  fnessref  36976  bj-ismooredr2  37860  pibt2  38171  fin2solem  38360  fin2so  38361  poimirlem2  38371  poimirlem14  38383  poimirlem25  38394  poimirlem26  38395  poimirlem29  38398  poimirlem30  38399  broucube  38403  heicant  38404  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  ex-ovoliunnfl  38412  mbfresfi  38415  cnambfre  38417  itg2addnclem  38420  itg2addnclem2  38421  itg2addnc  38423  ftc1anclem3  38444  ftc1anclem4  38445  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  indexdom  38484  filbcmb  38490  fdc  38495  incsequz  38498  metf1o  38505  caures  38510  bndss  38536  ismtycnv  38552  heiborlem1  38561  rrncmslem  38582  isdrngo2  38708  rngoisocnv  38731  unichnidl  38781  erimeq2  39511  ax12eq  39814  ax12el  39815  lshpset2N  39992  pmapglb2N  40644  pmapglb2xN  40645  pclfinN  40773  polval2N  40779  cdleme31fv2  41266  cdleme32fvcl  41313  cdleme48gfv  41410  tendoicl  41669  tendoipl  41670  diaglbN  41928  dochkr1  42351  dochkr1OLDN  42352  sumcubes  43188  expeq1d  43199  zaddcomlem  43351  zmulcomlem  43355  fiabv  43418  rhmcomulpsr  43428  evlselv  43435  fsuppind  43436  fsuppssind  43439  mhpind  43440  nacsfix  43557  eq0rabdioph  43621  diophren  43654  rencldnfilem  43661  pell1234qrdich  43702  jm2.24  43804  jm2.26lem3  43842  wepwsolem  43883  pwssplit4  43930  isnumbasgrplem3  43946  onexoegt  44085  onov0suclim  44115  cantnfresb  44165  omcl2  44174  ofoaid1  44199  ofoaid2  44200  grumnudlem  45109  cvgdvgrat  45137  ofsubid  45148  bcc0  45164  binomcxplemnn0  45173  uzwo4  45887  fiiuncl  45899  iunincfi  45926  nsstr  45927  rexanuz3  45928  iinssiin  45961  disjrnmpt2  46020  disjinfi  46024  choicefi  46031  difmap  46037  iunmapsn  46047  axccdom  46052  axccd  46058  rnmptlb  46072  rnmptbd2lem  46077  ssfiunibd  46142  supxrgelem  46167  suplesup  46169  xrlexaddrp  46182  xralrple2  46184  infxrunb2  46197  xralrple3  46203  xrralrecnnle  46212  xrralrecnnge  46219  supxrunb3  46228  unb2ltle  46243  rexabslelem  46246  supminfrnmpt  46273  infxrpnf  46274  supminfxr  46292  supminfxr2  46297  xrpnf  46313  pimxrneun  46316  cvgcaule  46319  iooiinicc  46372  ressioosup  46385  iooiinioc  46386  ressiooinf  46387  fsumsupp0  46408  divcnvg  46457  limcrecl  46459  sumnnodd  46460  islpcn  46467  lptre2pt  46468  limcresiooub  46470  limcresioolb  46471  limclner  46479  fnlimfvre  46502  allbutfifvre  46503  climinf3  46544  limsupmnflem  46548  limsupre3uzlem  46563  limsupreuzmpt  46567  climuzlem  46571  climisp  46574  climrescn  46576  climxrrelem  46577  climxrre  46578  climlimsupcex  46597  liminflelimsuplem  46603  limsupgtlem  46605  liminfvalxr  46611  liminfreuzlem  46630  liminfltlem  46632  liminflimsupclim  46635  xlimpnfxnegmnf  46642  liminflbuz2  46643  liminflimsupxrre  46645  cnrefiisplem  46657  xlimmnfvlem2  46661  xlimmnfv  46662  xlimpnfvlem2  46665  xlimpnfv  46666  xlimmnfmpt  46671  xlimpnfmpt  46672  climxlim2lem  46673  dfxlim2v  46675  xlimliminflimsup  46690  cncfuni  46714  icccncfext  46715  cncficcgt0  46716  cncfiooicclem1  46721  cncfiooiccre  46723  dvasinbx  46748  dvdsn1add  46767  dvnmul  46771  dvmptfprodlem  46772  dvnprodlem1  46774  dvnprodlem3  46776  iblspltprt  46801  itgioocnicc  46805  itgspltprt  46807  ismbl3  46814  stirlinglem5  46906  dirker2re  46920  dirkerper  46924  dirkertrigeq  46929  dirkercncflem2  46932  fourierdlem12  46947  fourierdlem15  46950  fourierdlem16  46951  fourierdlem20  46955  fourierdlem21  46956  fourierdlem22  46957  fourierdlem39  46974  fourierdlem40  46975  fourierdlem41  46976  fourierdlem42  46977  fourierdlem46  46980  fourierdlem49  46983  fourierdlem50  46984  fourierdlem57  46991  fourierdlem58  46992  fourierdlem59  46993  fourierdlem64  46998  fourierdlem65  46999  fourierdlem66  47000  fourierdlem68  47002  fourierdlem70  47004  fourierdlem71  47005  fourierdlem73  47007  fourierdlem78  47012  fourierdlem79  47013  fourierdlem80  47014  fourierdlem81  47015  fourierdlem82  47016  fourierdlem83  47017  fourierdlem87  47021  fourierdlem93  47027  fourierdlem95  47029  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  sqwvfoura  47056  fourierswlem  47058  elaa2lem  47061  etransclem13  47075  etransclem23  47085  etransclem24  47086  etransclem32  47094  etransclem38  47100  etransclem46  47108  qndenserrnbllem  47122  rrxsnicc  47128  ioorrnopnlem  47132  prsal  47146  intsal  47158  salexct  47162  dfsalgen2  47169  issalnnd  47173  sge0rnre  47192  sge0val  47194  sge0z  47203  sge0revalmpt  47206  sge0tsms  47208  sge0pr  47222  sge0resplit  47234  sge0split  47237  sge0splitmpt  47239  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0fodjrnlem  47244  sge0iunmpt  47246  sge0rpcpnf  47249  sge0ltfirpmpt2  47254  sge0isum  47255  sge0xaddlem1  47261  sge0xaddlem2  47262  sge0pnffsumgt  47270  sge0gtfsumgt  47271  sge0seq  47274  sge0reuz  47275  nnfoctbdjlem  47283  nnfoctbdj  47284  meadjun  47290  meadjiunlem  47293  voliunsge0lem  47300  meaiuninc3v  47312  omeiunltfirp  47347  carageniuncllem2  47350  caratheodorylem1  47354  caratheodorylem2  47355  caratheodory  47356  isomenndlem  47358  isomennd  47359  hoicvr  47376  volicorescl  47381  ovnsubaddlem2  47399  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvle  47428  ovnhoilem2  47430  hspdifhsp  47444  hoiqssbllem2  47451  hoiqssbllem3  47452  hspmbllem2  47455  ovnsubadd2lem  47473  ovolval4lem1  47477  vonvolmbl  47489  vonioo  47510  vonicc  47513  pimrecltpos  47536  issmfle  47573  smflimlem1  47599  smflimlem2  47600  smflimlem6  47604  smfresal  47616  smfrec  47617  smfmullem4  47622  smfpimcc  47636  smflimmpt  47638  smfsuplem1  47639  smfsuplem3  47641  smfsupmpt  47643  smfsupxr  47644  smfinflem  47645  smfinfmpt  47647  smflimsuplem4  47651  smflimsuplem5  47652  smflimsupmpt  47657  smfliminfmpt  47660  fsupdm  47670  finfdm  47674  smonoord  48265  lswn0  48344  poprelb  48424  fmtnoprmfac1  48468  fmtnofac2lem  48471  sbgoldbst  48694  isgrim  48798  gpgedgvtx0  48977  snlindsntorlem  49400  1arymaptf  49571  ipolubdm  49913  ipoglbdm  49916  setc1onsubc  50528  aacllem  50772