Theorem adantllr 719

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 482	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 680	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:  ad4ant13  751  ad4ant134  1175  ad5ant145  1371  oewordri  8507  marypha1lem  9317  rlimsqzlem  15556  fsumrlim  15718  fsumo1  15719  lcmdvds  16519  chnind  18527  dfgrp3lem  18951  tgcl  22884  neindisj  23032  neiptoptop  23046  isr0  23652  cnextcn  23982  ustuqtop4  24159  mpomulcn  24785  mbfsup  25592  itg2i1fseqle  25682  ditgsplit  25789  itgulm  26344  leibpi  26879  dchrisumlem3  27429  legov  28563  legov2  28564  legtrid  28569  colopp  28747  f1otrg  28849  cusgrsize2inds  29432  grpoidinvlem3  30486  grpoideu  30489  grporcan  30498  blocni  30785  normcan  31556  unoplin  31900  hmoplin  31922  nmophmi  32011  mdslmd3i  32312  chirredlem1  32370  chirredlem2  32371  mdsymlem5  32387  cdj1i  32413  opreu2reuALT  32456  fpwrelmap  32716  fsumiunle  32812  ccatf1  32930  wrdt2ind  32934  gsumwrd2dccatlem  33046  archiabllem1  33162  archiabl  33167  isarchiofld  33168  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem2  33215  ringlsmss1  33361  ringlsmss2  33362  nsgqusf1olem1  33378  nsgqusf1olem2  33379  nsgqusf1olem3  33380  rhmimaidl  33397  isprmidlc  33412  mplvrpmrhm  33577  esplyfv1  33590  fedgmul  33644  irngnzply1  33704  locfinreflem  33853  pstmxmet  33910  ordtconnlem1  33937  esumcvg  34099  esum2d  34106  esumiun  34107  ldgenpisyslem1  34176  omssubadd  34313  signstfvneq0  34585  circlemeth  34653  elicc3  36361  knoppcnlem9  36545  pibt2  37461  lindsenlbs  37654  matunitlindflem1  37655  poimirlem17  37676  poimirlem20  37679  poimirlem27  37686  poimirlem29  37688  poimir  37692  heicant  37694  itg2addnclem  37710  ftc1anclem5  37736  ftc1anclem6  37737  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  fzmul  37780  fdc  37784  fdc1  37785  incsequz2  37788  rrncmslem  37871  ghomco  37930  rngoisocnv  38020  ispridlc  38109  fiabv  42628  selvvvval  42677  fsuppind  42682  cvgdvgrat  44405  binomcxplemnotnn0  44448  founiiun0  45286  supxrge  45436  suplesup  45437  supxrunb3  45496  lptre2pt  45737  0ellimcdiv  45746  limclner  45748  limsuppnfdlem  45798  limsuppnflem  45807  limsupmnflem  45817  liminfreuzlem  45899  liminflimsupclim  45904  cnrefiisplem  45926  climxlim2lem  45942  xlimliminflimsup  45959  icccncfext  45984  cncfiooiccre  45992  fperdvper  46016  dvnprodlem2  46044  iblcncfioo  46075  stoweidlem35  46132  wallispilem3  46164  fourierdlem20  46224  fourierdlem34  46238  fourierdlem39  46243  fourierdlem42  46246  fourierdlem46  46249  fourierdlem48  46251  fourierdlem49  46252  fourierdlem63  46266  fourierdlem64  46267  fourierdlem73  46276  fourierdlem87  46290  fourierdlem97  46300  fourierdlem103  46306  fourierdlem104  46307  fourierdlem111  46314  etransclem32  46363  etransclem33  46364  etransclem35  46366  sge0cl  46478  sge0f1o  46479  sge0split  46506  sge0iunmptlemre  46512  sge0rpcpnf  46518  sge0xadd  46532  nnfoctbdjlem  46552  ismeannd  46564  omeiunltfirp  46616  hoidmvlelem3  46694  hoidmvle  46697  ovncvr2  46708  hspdifhsp  46713  hspmbllem2  46724  ovnsubadd2lem  46742  pimdecfgtioo  46814  pimincfltioo  46815  smflimlem1  46868  smflimmpt  46907  smfpimne2  46937  resccat  49174  aacllem  49901