Theorem adantlrr 721

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 482	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 681	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:  disjxiun  5104  2ndconst  8080  oelim  8498  odi  8543  marypha1lem  9384  dfac12lem2  10098  infunsdom  10166  isf34lem4  10330  distrlem1pr  10978  lcmgcdlem  16576  lcmdvds  16578  drsdirfi  18266  isacs3lem  18501  conjnmzb  19185  psgndif  21511  frlmsslsp  21705  metss2lem  24399  nghmcn  24633  bndth  24857  itg2monolem1  25651  dvmptfsum  25879  ply1divex  26042  itgulm  26317  rpvmasumlem  27398  dchrmusum2  27405  dchrisum0lem2  27429  dchrisum0lem3  27430  mulog2sumlem2  27446  pntibndlem3  27503  wwlksubclwwlk  29987  blocni  30734  superpos  32283  chirredlem2  32320  eulerpartlemgvv  34367  ballotlemfc0  34484  ballotlemfcc  34485  bj-finsumval0  37273  pibt2  37405  fin2solem  37600  matunitlindflem1  37610  poimirlem28  37642  heicant  37649  ftc1anclem6  37692  ftc1anc  37695  fdc  37739  incsequz  37742  ismtyres  37802  isdrngo2  37952  rngohomco  37968  keridl  38026  linepsubN  39746  pmapsub  39762  fsuppind  42578  mhpind  42582  mzpcompact2lem  42739  pellex  42823  monotuz  42930  unxpwdom3  43084  cantnfresb  43313  dssmapnvod  44009  radcnvrat  44303  fprodexp  45592  fprodabs2  45593  climxrrelem  45747  dvnprodlem1  45944  stoweidlem34  46032  fourierdlem42  46147  elaa2  46232  sge0iunmptlemfi  46411  aacllem  49790