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  5121  2ndconst  8105  oelim  8551  odi  8596  marypha1lem  9450  dfac12lem2  10164  infunsdom  10232  isf34lem4  10396  distrlem1pr  11044  lcmgcdlem  16630  lcmdvds  16632  drsdirfi  18322  isacs3lem  18557  conjnmzb  19241  psgndif  21567  frlmsslsp  21761  metss2lem  24455  nghmcn  24689  bndth  24913  itg2monolem1  25708  dvmptfsum  25936  ply1divex  26099  itgulm  26374  rpvmasumlem  27455  dchrmusum2  27462  dchrisum0lem2  27486  dchrisum0lem3  27487  mulog2sumlem2  27503  pntibndlem3  27560  wwlksubclwwlk  30044  blocni  30791  superpos  32340  chirredlem2  32377  eulerpartlemgvv  34413  ballotlemfc0  34530  ballotlemfcc  34531  bj-finsumval0  37308  pibt2  37440  fin2solem  37635  matunitlindflem1  37645  poimirlem28  37677  heicant  37684  ftc1anclem6  37727  ftc1anc  37730  fdc  37774  incsequz  37777  ismtyres  37837  isdrngo2  37987  rngohomco  38003  keridl  38061  linepsubN  39776  pmapsub  39792  fsuppind  42588  mhpind  42592  mzpcompact2lem  42749  pellex  42833  monotuz  42940  unxpwdom3  43094  cantnfresb  43323  dssmapnvod  44019  radcnvrat  44313  fprodexp  45603  fprodabs2  45604  climxrrelem  45758  dvnprodlem1  45955  stoweidlem34  46043  fourierdlem42  46158  elaa2  46243  sge0iunmptlemfi  46422  aacllem  49645