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

Proof of Theorem adantlrr

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5066  2ndconst  7799  oelim  8162  odi  8208  marypha1lem  8900  dfac12lem2  9573  infunsdom  9639  isf34lem4  9802  distrlem1pr  10450  lcmgcdlem  15953  lcmdvds  15955  drsdirfi  17551  isacs3lem  17779  conjnmzb  18396  psgndif  20749  frlmsslsp  20943  metss2lem  23124  nghmcn  23357  bndth  23565  itg2monolem1  24354  dvmptfsum  24575  ply1divex  24733  itgulm  24999  rpvmasumlem  26066  dchrmusum2  26073  dchrisum0lem2  26097  dchrisum0lem3  26098  mulog2sumlem2  26114  pntibndlem3  26171  wwlksubclwwlk  27840  blocni  28585  superpos  30134  chirredlem2  30171  eulerpartlemgvv  31638  ballotlemfc0  31754  ballotlemfcc  31755  bj-finsumval0  34571  pibt2  34702  fin2solem  34882  matunitlindflem1  34892  poimirlem28  34924  heicant  34931  ftc1anclem6  34976  ftc1anc  34979  fdc  35024  incsequz  35027  ismtyres  35090  isdrngo2  35240  rngohomco  35256  keridl  35314  linepsubN  36892  pmapsub  36908  mzpcompact2lem  39354  pellex  39438  monotuz  39544  unxpwdom3  39701  dssmapnvod  40372  radcnvrat  40652  fprodexp  41881  fprodabs2  41882  climxrrelem  42036  dvnprodlem1  42237  stoweidlem34  42326  fourierdlem42  42441  elaa2  42526  sge0iunmptlemfi  42702  aacllem  44909