Theorem adantlrr 718

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
adantlrr	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrr

Step	Hyp	Ref	Expression
1		simpl 483	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 678	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  disjxiun  5071  2ndconst  7941  oelim  8364  odi  8410  marypha1lem  9192  dfac12lem2  9900  infunsdom  9970  isf34lem4  10133  distrlem1pr  10781  lcmgcdlem  16311  lcmdvds  16313  drsdirfi  18023  isacs3lem  18260  conjnmzb  18869  psgndif  20807  frlmsslsp  21003  metss2lem  23667  nghmcn  23909  bndth  24121  itg2monolem1  24915  dvmptfsum  25139  ply1divex  25301  itgulm  25567  rpvmasumlem  26635  dchrmusum2  26642  dchrisum0lem2  26666  dchrisum0lem3  26667  mulog2sumlem2  26683  pntibndlem3  26740  wwlksubclwwlk  28422  blocni  29167  superpos  30716  chirredlem2  30753  eulerpartlemgvv  32343  ballotlemfc0  32459  ballotlemfcc  32460  bj-finsumval0  35456  pibt2  35588  fin2solem  35763  matunitlindflem1  35773  poimirlem28  35805  heicant  35812  ftc1anclem6  35855  ftc1anc  35858  fdc  35903  incsequz  35906  ismtyres  35966  isdrngo2  36116  rngohomco  36132  keridl  36190  linepsubN  37766  pmapsub  37782  fsuppind  40279  mhpind  40283  mzpcompact2lem  40573  pellex  40657  monotuz  40763  unxpwdom3  40920  dssmapnvod  41628  radcnvrat  41932  fprodexp  43135  fprodabs2  43136  climxrrelem  43290  dvnprodlem1  43487  stoweidlem34  43575  fourierdlem42  43690  elaa2  43775  sge0iunmptlemfi  43951  aacllem  46505