Theorem adantll 721

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ad2antlr  734  ad2ant2l  753  ad2ant2lr  755  ad5ant23  766  ad5ant24  767  ad5ant25  768  3adant1  1137  3ad2antl3  1195  ralcom2  3343  vtocl2d  3509  sbc2iegf  3799  sbcralt  3806  pofun  5547  poinxp  5702  xpdifid  6123  sossfld  6141  preddowncl  6287  tz7.7  6340  onfr  6353  ssimaex  6916  fsneq  6980  eqfnun  6982  fndmdif  6987  dffo4  7048  fompt  7063  fcompt  7079  fconst2g  7151  f1cofveqaeq  7205  isores3  7283  limsssuc  7794  el2mpocl  8029  1stconst  8043  2ndconst  8044  curry1  8047  curry2  8050  poseq  8102  soseq  8103  extmptsuppeq  8132  suppss  8138  suppss2  8144  onnseq  8278  oe0  8451  oesuclem  8454  oecl  8466  oaordi  8475  oawordri  8479  omordi  8495  omword2  8503  omlimcl  8507  odi  8508  omass  8509  oeoe  8529  nnaordi  8548  oaabs  8578  omsmolem  8587  eceqoveq  8763  mapsnd  8828  dom2lem  8933  sbthlem9  9027  rexdif1en  9089  isinf  9169  frfi  9189  fiint  9231  fodomfib  9233  fodomfibOLD  9235  fofinf1o  9236  marypha1lem  9340  ordiso2  9424  unwdomg  9493  xpwdomg  9494  frr1  9678  ac5num  9953  cff1  10175  cfcoflem  10189  infpssrlem4  10223  isf32lem9  10278  isf34lem7  10296  fin1a2lem13  10329  fin1a2s  10331  hsmexlem4  10346  axdc2lem  10365  zorn2lem6  10418  axpowndlem2  10516  inttsk  10692  tskuni  10701  nqereu  10847  prcdnq  10911  addclprlem2  10935  ltexpri  10961  prlem936  10965  reclem2pr  10966  axsup  11216  add4  11362  ltleadd  11628  lt2mul2div  12029  nn2ge  12199  zextle  12597  fnn0ind  12623  xrlttr  13086  ifle  13144  xnn0lem1lt  13191  xaddass  13196  xmulasslem3  13233  xlemul1a  13235  xadddilem  13241  xrsupsslem  13254  xrinfmsslem  13255  supxrunb1  13266  supxrunb2  13267  ixxin  13310  difreicc  13432  iccsplit  13433  iccshftr  13434  iccshftl  13436  iccdil  13438  icccntr  13440  fzaddel  13507  fzadd2  13508  fzrev  13536  modadd1  13862  modmul1  13881  fsuppmapnn0fiub  13948  mulexp  14058  expadd  14061  expmul  14064  expnbnd  14189  bccl  14279  hashdom  14336  prsshashgt1  14367  hashfacen  14411  brfi1uzind  14465  wrdnval  14502  swrdccat3blem  14696  revccat  14723  2shfti  15037  rexico  15311  cau3lem  15312  subcn2  15552  caucvgb  15637  iseraltlem1  15639  sumss  15681  fsumsplitsn  15701  incexclem  15796  supcvg  15816  mertenslem2  15845  fprodn0  15939  fprodsplitsn  15949  fprodle  15956  eftlcl  16069  reeftlcl  16070  rpnnen2lem6  16181  dvdsext  16285  3dvds  16295  sqoddm1div8z  16318  gcdcllem3  16465  dvdsexpim  16519  bezoutr1  16533  seq1st  16535  dvdslcm  16562  lcmeq0  16564  lcmcl  16565  lcmneg  16567  lcmdvds  16572  coprmgcdb  16613  dvdsprime  16651  pc2dvds  16845  prmpwdvds  16870  unbenlem  16874  infpnlem1  16876  1arith  16893  vdwmc2  16945  ramcl  16995  mrcuni  17582  isacs1i  17618  acsfn  17620  funcpropd  17864  curfcl  18193  curf2ndf  18208  resmgmhm  18674  resmgmhm2b  18676  mgmhmco  18677  mgmhmima  18678  resmhm  18783  resmhm2b  18785  mhmco  18786  pwsdiagmhm  18794  gsumwsubmcl  18800  gsumwspan  18809  pwmnd  18903  dfgrp2  18933  subgint  19121  ghmmhmb  19197  resghm  19202  cntzmhm  19311  symgextf1lem  19390  f1omvdconj  19416  dfod2  19534  gexdvds  19554  subgpgp  19567  sylow1lem3  19570  frgpnabllem1  19843  dprdfeq0  19994  rhmimasubrnglem  20541  cntzsubrng  20543  cntzsubr  20582  isdrng2  20719  islmodd  20860  lsslss  20955  reslmhm2b  21048  rngqiprngimfo  21298  psgnfix1  21577  psgndif  21581  copsgndif  21582  ocvocv  21650  frlmsslsp  21775  frlmlbs  21776  psrbaglefi  21905  psrdi  21943  psrass23l  21945  psrass23  21947  evlsvvval  22073  rhmcomulmpl  22104  selvcllem5  22119  psdmul  22158  mptcoe1fsupp  22204  psropprmul  22226  ply1coe  22288  mamudi  22390  mamudir  22391  mat1dimelbas  22458  scmatmulcl  22505  scmatfo  22517  mulmarep1gsum2  22561  mdetunilem7  22605  mdetunilem9  22607  gsummatr01lem3  22644  smadiadetlem3  22655  cpmadugsumlemF  22863  leordtval  23200  cnpnei  23251  cnco  23253  cnss1  23263  cmpsub  23387  hauscmplem  23393  dissnlocfin  23516  ptbasid  23562  tx2cn  23597  upxp  23610  txindis  23621  xkoptsub  23641  xkopt  23642  trfbas2  23830  filconn  23870  trfil2  23874  filssufilg  23898  ufileu  23906  fixufil  23909  ufilen  23917  rnelfmlem  23939  flimclsi  23965  hauspwpwf1  23974  fclsopn  24001  fclsfnflim  24014  fclscmpi  24016  alexsubALTlem4  24037  ptcmplem5  24043  tgpmulg  24080  subgtgp  24092  tgpt0  24106  tsmsxplem2  24141  metss  24495  metustfbas  24544  dscopn  24560  xrsmopn  24800  cncfss  24888  icoopnst  24928  iccpnfcnv  24933  icccvx  24939  evth  24948  phtpycc  24980  pcohtpylem  25008  lmmbrf  25251  fgcfil  25260  caucfil  25272  cfilres  25285  bcth3  25320  cmscsscms  25362  ovolfioo  25456  ovolficc  25457  voliunlem3  25541  volcn  25595  mbflimsup  25655  mbfi1fseqlem5  25708  itg2seq  25731  bddiblnc  25831  dvnff  25912  dvnadd  25918  cpnord  25924  c1liplem1  25985  plypf1  26199  plyaddlem1  26200  plymullem1  26201  coeeulem  26211  coeidlem  26224  dgrle  26230  dgrnznn  26234  plycjlem  26263  elqaalem3  26309  ulmcaulem  26381  ulmcau  26382  psergf  26399  psercn2  26410  efopn  26644  abscxpbnd  26739  leibpi  26928  isppw2  27100  muinv  27178  bposlem3  27271  gausslemma2dlem4  27354  pntrmax  27549  pntpbnd1  27571  qabvexp  27611  madebday  27914  mulsrid  28127  bdayons  28290  peano5n0s  28333  bdaypw2n0bndlem  28477  bdayfinlem  28500  eqeelen  28995  colinearalglem4  29000  axcgrid  29007  axsegconlem1  29008  axsegconlem3  29010  ax5seglem1  29019  ax5seglem2  29020  ax5seglem9  29028  axcontlem2  29056  cusgrfilem2  29547  vtxdgfisf  29567  usgr2pthlem  29853  uspgrn2crct  29898  crctcshwlkn0  29911  wwlksnext  29983  wwlksnextproplem3  30001  eupth2lem3lem4  30323  frgr3vlem1  30365  frgr3vlem2  30366  3vfriswmgrlem  30369  frgrwopreglem5  30413  numclwwlk3lem2  30476  grpoidinvlem3  30599  grpoidinv  30601  grpoideu  30602  nmoub3i  30866  nmlno0lem  30886  nmlnoubi  30889  ipasslem3  30926  ipblnfi  30948  hvaddsub4  31171  his35  31181  shsel3  31408  chj4  31628  spansncol  31661  chscllem2  31731  5oalem2  31748  3oalem2  31756  hoaddcl  31851  adjsym  31926  cnvadj  31985  hhcno  31997  hhcnf  31998  nmopub2tALT  32002  unoplin  32013  counop  32014  nmfnleub2  32019  hmoplin  32035  brafnmul  32044  nmlnop0iALT  32088  nmopun  32107  nmophmi  32124  riesz3i  32155  riesz1  32158  cnlnadjlem2  32161  cnlnadjlem6  32165  adjmul  32185  adjadd  32186  bra11  32201  cnvbraval  32203  kbass5  32213  kbass6  32214  leop2  32217  leopadd  32225  leopmuli  32226  leoptri  32229  leopnmid  32231  nmopleid  32232  pj3si  32300  hstel2  32312  cvcon3  32377  dmdmd  32393  dmdbr5  32401  mdsl0  32403  mdslmd1lem1  32418  mdslmd1lem2  32419  mdslmd3i  32425  superpos  32447  chirredlem2  32484  chirredlem3  32485  mdsymlem3  32498  mdsymlem5  32500  mdsymlem6  32501  sumdmdlem  32511  cdjreui  32525  cdj1i  32526  cdj3i  32534  foresf1o  32596  2ndimaxp  32742  abfmpel  32751  fcomptf  32754  fcnvgreu  32768  fdifsuppconst  32785  xrge0infss  32856  xnn0gt0  32865  sgn3da  32930  cycpm2tr  33204  elrgspnlem2  33328  elrgspnlem3  33329  intlidl  33507  rhmpreimaprmidl  33538  mplvrpmga  33741  psrmonmul  33746  esplyfval0  33760  vieta  33776  lssdimle  33804  mdetpmtr1  34019  cmpcref  34046  xrge0iifcnv  34129  zrhcntr  34175  esumcst  34259  hasheuni  34281  esum2dlem  34288  esum2d  34289  sigaclcu2  34316  insiga  34333  unelldsys  34354  measres  34418  measdivcst  34420  volfiniune  34426  ddemeas  34432  actfunsnf1o  34800  fnrelpredd  35287  fineqvac  35312  fineqvnttrclselem1  35317  sconnpi1  35482  cvmsss2  35517  satfv1lem  35605  fmlaomn0  35633  gonarlem  35637  mrsubco  35764  dfon2lem6  36029  hfext  36426  elicc3  36560  fnessref  36600  bj-ismooredr2  37483  pibt2  37794  fin2solem  37988  fin2so  37989  lindsenlbs  37997  matunitlindflem1  37998  matunitlindflem2  37999  poimirlem2  38004  poimirlem14  38016  poimirlem25  38027  poimirlem26  38028  poimirlem29  38031  poimirlem30  38032  broucube  38036  heicant  38037  mblfinlem2  38040  mblfinlem3  38041  mblfinlem4  38042  ex-ovoliunnfl  38045  mbfresfi  38048  cnambfre  38050  itg2addnclem  38053  itg2addnclem2  38054  itg2addnc  38056  ftc1anclem3  38077  ftc1anclem4  38078  ftc1anclem5  38079  ftc1anclem6  38080  ftc1anclem7  38081  ftc1anclem8  38082  ftc1anc  38083  indexdom  38116  filbcmb  38122  fdc  38127  incsequz  38130  metf1o  38137  caures  38142  bndss  38168  ismtycnv  38184  heiborlem1  38193  rrncmslem  38214  isdrngo2  38340  rngoisocnv  38363  unichnidl  38413  erimeq2  39145  ax12eq  39448  ax12el  39449  lshpset2N  39626  pmapglb2N  40278  pmapglb2xN  40279  pclfinN  40407  polval2N  40413  cdleme31fv2  40900  cdleme32fvcl  40947  cdleme48gfv  41044  tendoicl  41303  tendoipl  41304  diaglbN  41562  dochkr1  41985  dochkr1OLDN  41986  sumcubes  42805  expeq1d  42816  zaddcomlem  42968  zmulcomlem  42972  fiabv  43037  rhmcomulpsr  43047  evlselv  43054  fsuppind  43055  fsuppssind  43058  mhpind  43059  nacsfix  43176  eq0rabdioph  43240  diophren  43273  rencldnfilem  43280  pell1234qrdich  43321  jm2.24  43423  jm2.26lem3  43461  wepwsolem  43502  pwssplit4  43549  isnumbasgrplem3  43565  onexoegt  43704  onov0suclim  43734  cantnfresb  43784  omcl2  43793  ofoaid1  43818  ofoaid2  43819  grumnudlem  44744  cvgdvgrat  44772  ofsubid  44783  bcc0  44799  binomcxplemnn0  44808  uzwo4  45516  fiiuncl  45528  iunincfi  45555  nsstr  45556  rexanuz3  45557  iinssiin  45590  disjrnmpt2  45649  disjinfi  45653  choicefi  45660  difmap  45666  iunmapsn  45676  axccdom  45681  axccd  45687  rnmptlb  45701  rnmptbd2lem  45706  ssfiunibd  45771  supxrgelem  45796  suplesup  45798  xrlexaddrp  45811  xralrple2  45813  infxrunb2  45826  xralrple3  45832  xrralrecnnle  45841  xrralrecnnge  45848  supxrunb3  45857  unb2ltle  45872  rexabslelem  45875  supminfrnmpt  45902  infxrpnf  45903  supminfxr  45921  supminfxr2  45926  xrpnf  45942  pimxrneun  45945  cvgcaule  45948  iooiinicc  46001  ressioosup  46014  iooiinioc  46015  ressiooinf  46016  fsumsupp0  46037  divcnvg  46086  limcrecl  46088  sumnnodd  46089  islpcn  46096  lptre2pt  46097  limcresiooub  46099  limcresioolb  46100  limclner  46108  fnlimfvre  46131  allbutfifvre  46132  climinf3  46173  limsupmnflem  46177  limsupre3uzlem  46192  limsupreuzmpt  46196  climuzlem  46200  climisp  46203  climrescn  46205  climxrrelem  46206  climxrre  46207  climlimsupcex  46226  liminflelimsuplem  46232  limsupgtlem  46234  liminfvalxr  46240  liminfreuzlem  46259  liminfltlem  46261  liminflimsupclim  46264  xlimpnfxnegmnf  46271  liminflbuz2  46272  liminflimsupxrre  46274  cnrefiisplem  46286  xlimmnfvlem2  46290  xlimmnfv  46291  xlimpnfvlem2  46294  xlimpnfv  46295  xlimmnfmpt  46300  xlimpnfmpt  46301  climxlim2lem  46302  dfxlim2v  46304  xlimliminflimsup  46319  cncfuni  46343  icccncfext  46344  cncficcgt0  46345  cncfiooicclem1  46350  cncfiooiccre  46352  dvasinbx  46377  dvdsn1add  46396  dvnmul  46400  dvmptfprodlem  46401  dvnprodlem1  46403  dvnprodlem3  46405  iblspltprt  46430  itgioocnicc  46434  itgspltprt  46436  ismbl3  46443  stirlinglem5  46535  dirker2re  46549  dirkerper  46553  dirkertrigeq  46558  dirkercncflem2  46561  fourierdlem12  46576  fourierdlem15  46579  fourierdlem16  46580  fourierdlem20  46584  fourierdlem21  46585  fourierdlem22  46586  fourierdlem39  46603  fourierdlem40  46604  fourierdlem41  46605  fourierdlem42  46606  fourierdlem46  46609  fourierdlem49  46612  fourierdlem50  46613  fourierdlem57  46620  fourierdlem58  46621  fourierdlem59  46622  fourierdlem64  46627  fourierdlem65  46628  fourierdlem66  46629  fourierdlem68  46631  fourierdlem70  46633  fourierdlem71  46634  fourierdlem73  46636  fourierdlem78  46641  fourierdlem79  46642  fourierdlem80  46643  fourierdlem81  46644  fourierdlem82  46645  fourierdlem83  46646  fourierdlem87  46650  fourierdlem93  46656  fourierdlem95  46658  fourierdlem101  46664  fourierdlem103  46666  fourierdlem104  46667  fourierdlem111  46674  fourierdlem112  46675  sqwvfoura  46685  fourierswlem  46687  elaa2lem  46690  etransclem13  46704  etransclem23  46714  etransclem24  46715  etransclem32  46723  etransclem38  46729  etransclem46  46737  qndenserrnbllem  46751  rrxsnicc  46757  ioorrnopnlem  46761  prsal  46775  intsal  46787  salexct  46791  dfsalgen2  46798  issalnnd  46802  sge0rnre  46821  sge0val  46823  sge0z  46832  sge0revalmpt  46835  sge0tsms  46837  sge0pr  46851  sge0resplit  46863  sge0split  46866  sge0splitmpt  46868  sge0iunmptlemfi  46870  sge0iunmptlemre  46872  sge0fodjrnlem  46873  sge0iunmpt  46875  sge0rpcpnf  46878  sge0ltfirpmpt2  46883  sge0isum  46884  sge0xaddlem1  46890  sge0xaddlem2  46891  sge0pnffsumgt  46899  sge0gtfsumgt  46900  sge0seq  46903  sge0reuz  46904  nnfoctbdjlem  46912  nnfoctbdj  46913  meadjun  46919  meadjiunlem  46922  voliunsge0lem  46929  meaiuninc3v  46941  omeiunltfirp  46976  carageniuncllem2  46979  caratheodorylem1  46983  caratheodorylem2  46984  caratheodory  46985  isomenndlem  46987  isomennd  46988  hoicvr  47005  volicorescl  47010  ovnsubaddlem2  47028  hoidmvlelem2  47053  hoidmvlelem3  47054  hoidmvle  47057  ovnhoilem2  47059  hspdifhsp  47073  hoiqssbllem2  47080  hoiqssbllem3  47081  hspmbllem2  47084  ovnsubadd2lem  47102  ovolval4lem1  47106  vonvolmbl  47118  vonioo  47139  vonicc  47142  pimrecltpos  47165  issmfle  47202  smflimlem1  47228  smflimlem2  47229  smflimlem6  47233  smfresal  47245  smfrec  47246  smfmullem4  47251  smfpimcc  47265  smflimmpt  47267  smfsuplem1  47268  smfsuplem3  47270  smfsupmpt  47272  smfsupxr  47273  smfinflem  47274  smfinfmpt  47276  smflimsuplem4  47280  smflimsuplem5  47281  smflimsupmpt  47286  smfliminfmpt  47289  fsupdm  47299  finfdm  47303  smonoord  47854  lswn0  47933  poprelb  48013  fmtnoprmfac1  48057  fmtnofac2lem  48060  sbgoldbst  48283  isgrim  48387  gpgedgvtx0  48566  snlindsntorlem  48975  1arymaptf  49146  ipolubdm  49491  ipoglbdm  49494  setc1onsubc  50106  aacllem  50305