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  5090  2ndconst  8037  oelim  8455  odi  8500  marypha1lem  9324  dfac12lem2  10043  infunsdom  10111  isf34lem4  10275  distrlem1pr  10923  lcmgcdlem  16519  lcmdvds  16521  drsdirfi  18213  isacs3lem  18450  conjnmzb  19167  psgndif  21541  frlmsslsp  21735  metss2lem  24427  nghmcn  24661  bndth  24885  itg2monolem1  25679  dvmptfsum  25907  ply1divex  26070  itgulm  26345  rpvmasumlem  27426  dchrmusum2  27433  dchrisum0lem2  27457  dchrisum0lem3  27458  mulog2sumlem2  27474  pntibndlem3  27531  wwlksubclwwlk  30040  blocni  30787  superpos  32336  chirredlem2  32373  eulerpartlemgvv  34410  ballotlemfc0  34527  ballotlemfcc  34528  bj-finsumval0  37350  pibt2  37482  fin2solem  37666  matunitlindflem1  37676  poimirlem28  37708  heicant  37715  ftc1anclem6  37758  ftc1anc  37761  fdc  37805  incsequz  37808  ismtyres  37868  isdrngo2  38018  rngohomco  38034  keridl  38092  linepsubN  39871  pmapsub  39887  fsuppind  42708  mhpind  42712  mzpcompact2lem  42868  pellex  42952  monotuz  43058  unxpwdom3  43212  cantnfresb  43441  dssmapnvod  44137  radcnvrat  44431  fprodexp  45718  fprodabs2  45719  climxrrelem  45871  dvnprodlem1  46068  stoweidlem34  46156  fourierdlem42  46271  elaa2  46356  sge0iunmptlemfi  46535  aacllem  49926