Theorem adantllr 732

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantllr	⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 693	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:  ad4ant13  764  ad4ant134  1193  ad5ant145  1396  oewordri  8584  marypha1lem  9407  ccatf1  14660  rlimsqzlem  15740  fsumrlim  15902  fsumo1  15903  lcmdvds  16704  chnind  18715  dfgrp3lem  19167  isprmidlc  21541  lindsenlbs  22070  selvvvval  22364  matunitlindflem1  22907  tgcl  23200  neindisj  23348  neiptoptop  23362  isr0  23969  cnextcn  24299  ustuqtop4  24476  mpomulcn  25101  mbfsup  25898  itg2i1fseqle  25988  ditgsplit  26095  itgulm  26651  leibpi  27187  dchrisumlem3  27735  legov  28935  legov2  28936  legtrid  28941  colopp  29134  perpprlng  29315  f1otrg  29335  cusgrsize2inds  29921  grpoidinvlem3  30995  grpoideu  30998  grporcan  31007  blocni  31294  normcan  32065  unoplin  32409  hmoplin  32431  nmophmi  32520  mdslmd3i  32821  chirredlem1  32879  chirredlem2  32880  mdsymlem5  32896  cdj1i  32922  opreu2reuALT  32960  fpwrelmap  33212  fsumiunle  33307  wrdt2ind  33403  suppgsumssiun  33520  gsumwrd2dccatlem  33525  archiabllem1  33641  archiabl  33646  isarchiofld  33647  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem4  33693  elrgspnsubrunlem2  33696  ringlsmss1  33835  ringlsmss2  33836  nsgqusf1olem1  33850  nsgqusf1olem2  33851  nsgqusf1olem3  33852  rhmimaidl  33868  mplvrpmrhm  34065  esplyfv1  34087  esplyfval1  34091  fedgmul  34149  irngnzply1  34209  locfinreflem  34358  pstmxmet  34415  ordtconnlem1  34442  esumcvg  34604  esum2d  34611  esumiun  34612  ldgenpisyslem1  34682  omssubadd  34819  signstfvneq0  35088  circlemeth  35156  elicc3  36944  knoppcnlem9  37206  pibt2  38179  poimirlem17  38394  poimirlem20  38397  poimirlem27  38404  poimirlem29  38406  poimir  38410  heicant  38412  itg2addnclem  38428  ftc1anclem5  38454  ftc1anclem6  38455  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  fzmul  38499  fdc  38503  fdc1  38504  incsequz2  38507  rrncmslem  38590  ghomco  38649  rngoisocnv  38739  ispridlc  38828  fiabv  43426  fsuppind  43444  cvgdvgrat  45145  binomcxplemnotnn0  45188  founiiun0  46030  supxrge  46176  suplesup  46177  supxrunb3  46236  lptre2pt  46476  0ellimcdiv  46485  limclner  46487  limsuppnfdlem  46537  limsuppnflem  46546  limsupmnflem  46556  liminfreuzlem  46638  liminflimsupclim  46643  cnrefiisplem  46665  climxlim2lem  46681  xlimliminflimsup  46698  icccncfext  46723  cncfiooiccre  46731  fperdvper  46755  dvnprodlem2  46783  iblcncfioo  46814  stoweidlem35  46871  wallispilem3  46903  fourierdlem20  46963  fourierdlem34  46977  fourierdlem39  46982  fourierdlem42  46985  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem63  47005  fourierdlem64  47006  fourierdlem73  47015  fourierdlem87  47029  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  etransclem32  47102  etransclem33  47103  etransclem35  47105  sge0cl  47217  sge0f1o  47218  sge0split  47245  sge0iunmptlemre  47251  sge0rpcpnf  47257  sge0xadd  47271  nnfoctbdjlem  47291  ismeannd  47303  omeiunltfirp  47355  hoidmvlelem3  47433  hoidmvle  47436  ovncvr2  47447  hspdifhsp  47452  hspmbllem2  47463  ovnsubadd2lem  47481  pimdecfgtioo  47553  pimincfltioo  47554  smflimlem1  47607  smflimmpt  47646  smfpimne2  47676  resccat  50008  aacllem  50780