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  5145  2ndconst  8125  oelim  8571  odi  8616  marypha1lem  9471  dfac12lem2  10183  infunsdom  10251  isf34lem4  10415  distrlem1pr  11063  lcmgcdlem  16640  lcmdvds  16642  drsdirfi  18363  isacs3lem  18600  conjnmzb  19284  psgndif  21638  frlmsslsp  21834  metss2lem  24540  nghmcn  24782  bndth  25004  itg2monolem1  25800  dvmptfsum  26028  ply1divex  26191  itgulm  26466  rpvmasumlem  27546  dchrmusum2  27553  dchrisum0lem2  27577  dchrisum0lem3  27578  mulog2sumlem2  27594  pntibndlem3  27651  wwlksubclwwlk  30087  blocni  30834  superpos  32383  chirredlem2  32420  eulerpartlemgvv  34358  ballotlemfc0  34474  ballotlemfcc  34475  bj-finsumval0  37268  pibt2  37400  fin2solem  37593  matunitlindflem1  37603  poimirlem28  37635  heicant  37642  ftc1anclem6  37685  ftc1anc  37688  fdc  37732  incsequz  37735  ismtyres  37795  isdrngo2  37945  rngohomco  37961  keridl  38019  linepsubN  39735  pmapsub  39751  fsuppind  42577  mhpind  42581  mzpcompact2lem  42739  pellex  42823  monotuz  42930  unxpwdom3  43084  cantnfresb  43314  dssmapnvod  44010  radcnvrat  44310  fprodexp  45550  fprodabs2  45551  climxrrelem  45705  dvnprodlem1  45902  stoweidlem34  45990  fourierdlem42  46105  elaa2  46190  sge0iunmptlemfi  46369  aacllem  49032