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  3344  vtocl2d  3516  sbc2iegf  3812  sbcralt  3819  pofun  5547  poinxp  5702  xpdifid  6123  sossfld  6141  preddowncl  6287  tz7.7  6340  onfr  6353  ssimaex  6916  eqfnun  6979  fndmdif  6984  dffo4  7045  fompt  7060  fcompt  7075  fconst2g  7146  f1cofveqaeq  7200  isores3  7278  limsssuc  7789  el2mpocl  8025  1stconst  8039  2ndconst  8040  curry1  8043  curry2  8046  poseq  8097  soseq  8098  extmptsuppeq  8127  suppss  8133  suppss2  8139  onnseq  8273  oe0  8446  oesuclem  8449  oecl  8461  oaordi  8470  oawordri  8474  omordi  8490  omword2  8498  omlimcl  8502  odi  8503  omass  8504  oeoe  8523  nnaordi  8542  oaabs  8572  omsmolem  8581  eceqoveq  8755  mapsnd  8820  dom2lem  8925  sbthlem9  9019  rexdif1en  9081  isinf  9160  frfi  9180  fiint  9222  fodomfib  9224  fodomfibOLD  9226  fofinf1o  9227  marypha1lem  9328  ordiso2  9412  unwdomg  9481  xpwdomg  9482  frr1  9663  ac5num  9938  cff1  10160  cfcoflem  10174  infpssrlem4  10208  isf32lem9  10263  isf34lem7  10281  fin1a2lem13  10314  fin1a2s  10316  hsmexlem4  10331  axdc2lem  10350  zorn2lem6  10403  axpowndlem2  10500  inttsk  10676  tskuni  10685  nqereu  10831  prcdnq  10895  addclprlem2  10919  ltexpri  10945  prlem936  10949  reclem2pr  10950  axsup  11199  add4  11345  ltleadd  11611  lt2mul2div  12011  nn2ge  12163  zextle  12556  fnn0ind  12582  xrlttr  13045  ifle  13103  xnn0lem1lt  13150  xaddass  13155  xmulasslem3  13192  xlemul1a  13194  xadddilem  13200  xrsupsslem  13213  xrinfmsslem  13214  supxrunb1  13225  supxrunb2  13226  ixxin  13269  difreicc  13391  iccsplit  13392  iccshftr  13393  iccshftl  13395  iccdil  13397  icccntr  13399  fzaddel  13465  fzadd2  13466  fzrev  13494  modadd1  13819  modmul1  13838  fsuppmapnn0fiub  13905  mulexp  14015  expadd  14018  expmul  14021  expnbnd  14146  bccl  14236  hashdom  14293  prsshashgt1  14324  hashfacen  14368  brfi1uzind  14422  wrdnval  14459  swrdccat3blem  14653  revccat  14680  2shfti  14994  rexico  15268  cau3lem  15269  subcn2  15509  caucvgb  15594  iseraltlem1  15596  sumss  15638  fsumsplitsn  15658  incexclem  15750  supcvg  15770  mertenslem2  15799  fprodn0  15893  fprodsplitsn  15903  fprodle  15910  eftlcl  16023  reeftlcl  16024  rpnnen2lem6  16135  dvdsext  16239  3dvds  16249  sqoddm1div8z  16272  gcdcllem3  16419  dvdsexpim  16473  bezoutr1  16487  seq1st  16489  dvdslcm  16516  lcmeq0  16518  lcmcl  16519  lcmneg  16521  lcmdvds  16526  coprmgcdb  16567  dvdsprime  16605  pc2dvds  16798  prmpwdvds  16823  unbenlem  16827  infpnlem1  16829  1arith  16846  vdwmc2  16898  ramcl  16948  mrcuni  17535  isacs1i  17571  acsfn  17573  funcpropd  17817  curfcl  18146  curf2ndf  18161  resmgmhm  18627  resmgmhm2b  18629  mgmhmco  18630  mgmhmima  18631  resmhm  18736  resmhm2b  18738  mhmco  18739  pwsdiagmhm  18747  gsumwsubmcl  18753  gsumwspan  18762  pwmnd  18853  dfgrp2  18883  subgint  19071  ghmmhmb  19147  resghm  19152  cntzmhm  19261  symgextf1lem  19340  f1omvdconj  19366  dfod2  19484  gexdvds  19504  subgpgp  19517  sylow1lem3  19520  frgpnabllem1  19793  dprdfeq0  19944  rhmimasubrnglem  20489  cntzsubrng  20491  cntzsubr  20530  isdrng2  20667  islmodd  20808  lsslss  20903  reslmhm2b  20997  rngqiprngimfo  21247  psgnfix1  21544  psgndif  21548  copsgndif  21549  ocvocv  21617  frlmsslsp  21742  frlmlbs  21743  psrbaglefi  21873  psrdi  21911  psrass23l  21913  psrass23  21915  evlsvvval  22039  psdmul  22100  mptcoe1fsupp  22147  psropprmul  22169  ply1coe  22233  rhmcomulmpl  22317  mamudi  22338  mamudir  22339  mat1dimelbas  22406  scmatmulcl  22453  scmatfo  22465  mulmarep1gsum2  22509  mdetunilem7  22553  mdetunilem9  22555  gsummatr01lem3  22592  smadiadetlem3  22603  cpmadugsumlemF  22811  leordtval  23148  cnpnei  23199  cnco  23201  cnss1  23211  cmpsub  23335  hauscmplem  23341  dissnlocfin  23464  ptbasid  23510  tx2cn  23545  upxp  23558  txindis  23569  xkoptsub  23589  xkopt  23590  trfbas2  23778  filconn  23818  trfil2  23822  filssufilg  23846  ufileu  23854  fixufil  23857  ufilen  23865  rnelfmlem  23887  flimclsi  23913  hauspwpwf1  23922  fclsopn  23949  fclsfnflim  23962  fclscmpi  23964  alexsubALTlem4  23985  ptcmplem5  23991  tgpmulg  24028  subgtgp  24040  tgpt0  24054  tsmsxplem2  24089  metss  24443  metustfbas  24492  dscopn  24508  xrsmopn  24748  cncfss  24839  icoopnst  24883  iccpnfcnv  24889  icccvx  24895  evth  24905  phtpycc  24937  pcohtpylem  24966  lmmbrf  25209  fgcfil  25218  caucfil  25230  cfilres  25243  bcth3  25278  cmscsscms  25320  ovolfioo  25415  ovolficc  25416  voliunlem3  25500  volcn  25554  mbflimsup  25614  mbfi1fseqlem5  25667  itg2seq  25690  bddiblnc  25790  dvnff  25872  dvnadd  25878  cpnord  25884  c1liplem1  25948  plypf1  26164  plyaddlem1  26165  plymullem1  26166  coeeulem  26176  coeidlem  26189  dgrle  26195  dgrnznn  26199  plycjlem  26229  elqaalem3  26276  ulmcaulem  26350  ulmcau  26351  psergf  26368  psercn2  26379  psercn2OLD  26380  efopn  26614  abscxpbnd  26710  leibpi  26899  isppw2  27072  muinv  27150  bposlem3  27244  gausslemma2dlem4  27327  pntrmax  27522  pntpbnd1  27544  qabvexp  27584  madebday  27865  mulsrid  28072  bdayon  28229  peano5n0s  28268  zs12bday  28414  eqeelen  28903  colinearalglem4  28908  axcgrid  28915  axsegconlem1  28916  axsegconlem3  28918  ax5seglem1  28927  ax5seglem2  28928  ax5seglem9  28936  axcontlem2  28964  cusgrfilem2  29456  vtxdgfisf  29476  usgr2pthlem  29762  uspgrn2crct  29807  crctcshwlkn0  29820  wwlksnext  29892  wwlksnextproplem3  29910  eupth2lem3lem4  30232  frgr3vlem1  30274  frgr3vlem2  30275  3vfriswmgrlem  30278  frgrwopreglem5  30322  numclwwlk3lem2  30385  grpoidinvlem3  30507  grpoidinv  30509  grpoideu  30510  nmoub3i  30774  nmlno0lem  30794  nmlnoubi  30797  ipasslem3  30834  ipblnfi  30856  hvaddsub4  31079  his35  31089  shsel3  31316  chj4  31536  spansncol  31569  chscllem2  31639  5oalem2  31656  3oalem2  31664  hoaddcl  31759  adjsym  31834  cnvadj  31893  hhcno  31905  hhcnf  31906  nmopub2tALT  31910  unoplin  31921  counop  31922  nmfnleub2  31927  hmoplin  31943  brafnmul  31952  nmlnop0iALT  31996  nmopun  32015  nmophmi  32032  riesz3i  32063  riesz1  32066  cnlnadjlem2  32069  cnlnadjlem6  32073  adjmul  32093  adjadd  32094  bra11  32109  cnvbraval  32111  kbass5  32121  kbass6  32122  leop2  32125  leopadd  32133  leopmuli  32134  leoptri  32137  leopnmid  32139  nmopleid  32140  pj3si  32208  hstel2  32220  cvcon3  32285  dmdmd  32301  dmdbr5  32309  mdsl0  32311  mdslmd1lem1  32326  mdslmd1lem2  32327  mdslmd3i  32333  superpos  32355  chirredlem2  32392  chirredlem3  32393  mdsymlem3  32406  mdsymlem5  32408  mdsymlem6  32409  sumdmdlem  32419  cdjreui  32433  cdj1i  32434  cdj3i  32442  foresf1o  32505  2ndimaxp  32650  abfmpel  32659  fcomptf  32662  fcnvgreu  32677  fdifsuppconst  32694  xrge0infss  32768  xnn0gt0  32777  sgn3da  32843  cycpm2tr  33129  elrgspnlem2  33253  elrgspnlem3  33254  intlidl  33429  rhmpreimaprmidl  33460  mplvrpmga  33638  esplyfval0  33650  vieta  33664  lssdimle  33692  mdetpmtr1  33908  cmpcref  33935  xrge0iifcnv  34018  zrhcntr  34064  esumcst  34148  hasheuni  34170  esum2dlem  34177  esum2d  34178  sigaclcu2  34205  insiga  34222  unelldsys  34243  measres  34307  measdivcst  34309  volfiniune  34315  ddemeas  34321  actfunsnf1o  34689  fnrelpredd  35174  fineqvac  35211  fineqvnttrclselem1  35213  sconnpi1  35355  cvmsss2  35390  satfv1lem  35478  fmlaomn0  35506  gonarlem  35510  mrsubco  35637  dfon2lem6  35902  hfext  36299  elicc3  36433  fnessref  36473  bj-ismooredr2  37227  pibt2  37534  fin2solem  37719  fin2so  37720  lindsenlbs  37728  matunitlindflem1  37729  matunitlindflem2  37730  poimirlem2  37735  poimirlem14  37747  poimirlem25  37758  poimirlem26  37759  poimirlem29  37762  poimirlem30  37763  broucube  37767  heicant  37768  mblfinlem2  37771  mblfinlem3  37772  mblfinlem4  37773  ex-ovoliunnfl  37776  mbfresfi  37779  cnambfre  37781  itg2addnclem  37784  itg2addnclem2  37785  itg2addnc  37787  ftc1anclem3  37808  ftc1anclem4  37809  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  indexdom  37847  filbcmb  37853  fdc  37858  incsequz  37861  metf1o  37868  caures  37873  bndss  37899  ismtycnv  37915  heiborlem1  37924  rrncmslem  37945  isdrngo2  38071  rngoisocnv  38094  unichnidl  38144  erimeq2  38849  ax12eq  39113  ax12el  39114  lshpset2N  39291  pmapglb2N  39943  pmapglb2xN  39944  pclfinN  40072  polval2N  40078  cdleme31fv2  40565  cdleme32fvcl  40612  cdleme48gfv  40709  tendoicl  40968  tendoipl  40969  diaglbN  41227  dochkr1  41650  dochkr1OLDN  41651  sumcubes  42483  expeq1d  42494  zaddcomlem  42633  zmulcomlem  42637  fiabv  42706  rhmcomulpsr  42719  selvcllem5  42740  evlselv  42745  fsuppind  42748  fsuppssind  42751  mhpind  42752  nacsfix  42869  eq0rabdioph  42933  diophren  42970  rencldnfilem  42977  pell1234qrdich  43018  jm2.24  43120  jm2.26lem3  43158  wepwsolem  43199  pwssplit4  43246  isnumbasgrplem3  43262  onexoegt  43401  onov0suclim  43431  cantnfresb  43481  omcl2  43490  ofoaid1  43515  ofoaid2  43516  grumnudlem  44442  cvgdvgrat  44470  ofsubid  44481  bcc0  44497  binomcxplemnn0  44506  uzwo4  45214  fiiuncl  45226  iunincfi  45254  nsstr  45255  rexanuz3  45256  iinssiin  45289  disjrnmpt2  45348  disjinfi  45352  choicefi  45360  fsneq  45366  difmap  45367  iunmapsn  45377  axccdom  45382  axccd  45389  rnmptlb  45403  rnmptbd2lem  45408  ssfiunibd  45473  supxrgelem  45498  suplesup  45500  xrlexaddrp  45513  xralrple2  45515  infxrunb2  45528  xralrple3  45534  xrralrecnnle  45543  xrralrecnnge  45550  supxrunb3  45559  unb2ltle  45575  rexabslelem  45578  supminfrnmpt  45605  infxrpnf  45606  supminfxr  45624  supminfxr2  45629  xrpnf  45645  pimxrneun  45648  cvgcaule  45651  iooiinicc  45704  ressioosup  45717  iooiinioc  45718  ressiooinf  45719  fsumsupp0  45740  divcnvg  45789  limcrecl  45791  sumnnodd  45792  islpcn  45799  lptre2pt  45800  limcresiooub  45802  limcresioolb  45803  limclner  45811  fnlimfvre  45834  allbutfifvre  45835  climinf3  45876  limsupmnflem  45880  limsupre3uzlem  45895  limsupreuzmpt  45899  climuzlem  45903  climisp  45906  climrescn  45908  climxrrelem  45909  climxrre  45910  climlimsupcex  45929  liminflelimsuplem  45935  limsupgtlem  45937  liminfvalxr  45943  liminfreuzlem  45962  liminfltlem  45964  liminflimsupclim  45967  xlimpnfxnegmnf  45974  liminflbuz2  45975  liminflimsupxrre  45977  cnrefiisplem  45989  xlimmnfvlem2  45993  xlimmnfv  45994  xlimpnfvlem2  45997  xlimpnfv  45998  xlimmnfmpt  46003  xlimpnfmpt  46004  climxlim2lem  46005  dfxlim2v  46007  xlimliminflimsup  46022  cncfuni  46046  icccncfext  46047  cncficcgt0  46048  cncfiooicclem1  46053  cncfiooiccre  46055  dvasinbx  46080  dvdsn1add  46099  dvnmul  46103  dvmptfprodlem  46104  dvnprodlem1  46106  dvnprodlem3  46108  iblspltprt  46133  itgioocnicc  46137  itgspltprt  46139  ismbl3  46146  stirlinglem5  46238  dirker2re  46252  dirkerper  46256  dirkertrigeq  46261  dirkercncflem2  46264  fourierdlem12  46279  fourierdlem15  46282  fourierdlem16  46283  fourierdlem20  46287  fourierdlem21  46288  fourierdlem22  46289  fourierdlem39  46306  fourierdlem40  46307  fourierdlem41  46308  fourierdlem42  46309  fourierdlem46  46312  fourierdlem49  46315  fourierdlem50  46316  fourierdlem57  46323  fourierdlem58  46324  fourierdlem59  46325  fourierdlem64  46330  fourierdlem65  46331  fourierdlem66  46332  fourierdlem68  46334  fourierdlem70  46336  fourierdlem71  46337  fourierdlem73  46339  fourierdlem78  46344  fourierdlem79  46345  fourierdlem80  46346  fourierdlem81  46347  fourierdlem82  46348  fourierdlem83  46349  fourierdlem87  46353  fourierdlem93  46359  fourierdlem95  46361  fourierdlem101  46367  fourierdlem103  46369  fourierdlem104  46370  fourierdlem111  46377  fourierdlem112  46378  sqwvfoura  46388  fourierswlem  46390  elaa2lem  46393  etransclem13  46407  etransclem23  46417  etransclem24  46418  etransclem32  46426  etransclem38  46432  etransclem46  46440  qndenserrnbllem  46454  rrxsnicc  46460  ioorrnopnlem  46464  prsal  46478  intsal  46490  salexct  46494  dfsalgen2  46501  issalnnd  46505  sge0rnre  46524  sge0val  46526  sge0z  46535  sge0revalmpt  46538  sge0tsms  46540  sge0pr  46554  sge0resplit  46566  sge0split  46569  sge0splitmpt  46571  sge0iunmptlemfi  46573  sge0iunmptlemre  46575  sge0fodjrnlem  46576  sge0iunmpt  46578  sge0rpcpnf  46581  sge0ltfirpmpt2  46586  sge0isum  46587  sge0xaddlem1  46593  sge0xaddlem2  46594  sge0pnffsumgt  46602  sge0gtfsumgt  46603  sge0seq  46606  sge0reuz  46607  nnfoctbdjlem  46615  nnfoctbdj  46616  meadjun  46622  meadjiunlem  46625  voliunsge0lem  46632  meaiuninc3v  46644  omeiunltfirp  46679  carageniuncllem2  46682  caratheodorylem1  46686  caratheodorylem2  46687  caratheodory  46688  isomenndlem  46690  isomennd  46691  hoicvr  46708  volicorescl  46713  ovnsubaddlem2  46731  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvle  46760  ovnhoilem2  46762  hspdifhsp  46776  hoiqssbllem2  46783  hoiqssbllem3  46784  hspmbllem2  46787  ovnsubadd2lem  46805  ovolval4lem1  46809  vonvolmbl  46821  vonioo  46842  vonicc  46845  pimrecltpos  46868  issmfle  46905  smflimlem1  46931  smflimlem2  46932  smflimlem6  46936  smfresal  46948  smfrec  46949  smfmullem4  46954  smfpimcc  46968  smflimmpt  46970  smfsuplem1  46971  smfsuplem3  46973  smfsupmpt  46975  smfsupxr  46976  smfinflem  46977  smfinfmpt  46979  smflimsuplem4  46983  smflimsuplem5  46984  smflimsupmpt  46989  smfliminfmpt  46992  fsupdm  47002  finfdm  47006  smonoord  47533  lswn0  47606  poprelb  47686  fmtnoprmfac1  47727  fmtnofac2lem  47730  sbgoldbst  47940  isgrim  48044  gpgedgvtx0  48223  snlindsntorlem  48632  1arymaptf  48803  ipolubdm  49148  ipoglbdm  49151  setc1onsubc  49763  aacllem  49962