Theorem adantllr 712

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 476	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 672	1 ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  adantl3r  758  ad4ant134  1223  ad5ant145  1492  r19.29an  3287  oewordri  7939  marypha1lem  8608  gruwun  9950  lemul12b  11210  rlimsqzlem  14756  fsumrlim  14917  fsumo1  14918  lcmdvds  15694  isacs2  16666  dfgrp3lem  17867  tgcl  21144  neindisj  21292  neiptoptop  21306  isr0  21911  cnextcn  22241  ustuqtop4  22418  metss  22683  mbfsup  23830  itg2i1fseqle  23920  ditgsplit  24024  itgulm  24561  leibpi  25082  dchrisumlem3  25593  iscgrglt  25826  legov  25897  legov2  25898  legtrid  25903  colopp  26078  f1otrg  26170  cusgrsize2inds  26751  grpoidinvlem3  27916  grpoideu  27919  grporcan  27928  blocni  28215  normcan  28990  unoplin  29334  hmoplin  29356  nmophmi  29445  mdslmd3i  29746  chirredlem1  29804  chirredlem2  29805  mdsymlem5  29821  cdj1i  29847  fpwrelmap  30056  fsumiunle  30122  archiabllem1  30292  archiabl  30297  isarchiofld  30362  locfinreflem  30452  pstmxmet  30485  ordtconnlem1  30515  esumcvg  30693  esum2d  30700  esumiun  30701  ldgenpisyslem1  30771  omssubadd  30907  signstfvneq0  31197  circlemeth  31267  elicc3  32850  knoppcnlem9  33024  lindsenlbs  33948  matunitlindflem1  33949  poimirlem17  33970  poimirlem20  33973  poimirlem27  33980  poimirlem29  33982  poimir  33986  heicant  33988  itg2addnclem  34004  ftc1anclem5  34032  ftc1anclem6  34033  ftc1anclem7  34034  ftc1anclem8  34035  ftc1anc  34036  fzmul  34079  fdc  34083  fdc1  34084  incsequz2  34087  rrncmslem  34173  ghomco  34232  rngoisocnv  34322  ispridlc  34411  cvgdvgrat  39352  binomcxplemnotnn0  39395  founiiun0  40185  supxrge  40351  suplesup  40352  supxrunb3  40418  lptre2pt  40667  0ellimcdiv  40676  limclner  40678  limsuppnfdlem  40728  limsuppnflem  40737  limsupmnflem  40747  liminfreuzlem  40829  liminflimsupclim  40834  cnrefiisplem  40850  climxlim2lem  40866  icccncfext  40895  cncfiooiccre  40903  fperdvper  40928  dvnprodlem2  40957  iblcncfioo  40988  stoweidlem35  41046  wallispilem3  41078  fourierdlem20  41138  fourierdlem34  41152  fourierdlem39  41157  fourierdlem42  41160  fourierdlem46  41163  fourierdlem48  41165  fourierdlem49  41166  fourierdlem63  41180  fourierdlem64  41181  fourierdlem73  41190  fourierdlem87  41204  fourierdlem97  41214  fourierdlem103  41220  fourierdlem104  41221  fourierdlem111  41228  etransclem32  41277  etransclem33  41278  etransclem35  41280  sge0cl  41389  sge0f1o  41390  sge0split  41417  sge0iunmptlemre  41423  sge0rpcpnf  41429  sge0xadd  41443  nnfoctbdjlem  41463  ismeannd  41475  omeiunltfirp  41527  hoidmvlelem3  41605  hoidmvle  41608  ovncvr2  41619  hspdifhsp  41624  hspmbllem2  41635  ovnsubadd2lem  41653  pimdecfgtioo  41721  pimincfltioo  41722  smflimlem1  41773  smflimmpt  41810  aacllem  43443