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  5088  2ndconst  8031  oelim  8449  odi  8494  marypha1lem  9317  dfac12lem2  10033  infunsdom  10101  isf34lem4  10265  distrlem1pr  10913  lcmgcdlem  16514  lcmdvds  16516  drsdirfi  18208  isacs3lem  18445  conjnmzb  19163  psgndif  21537  frlmsslsp  21731  metss2lem  24424  nghmcn  24658  bndth  24882  itg2monolem1  25676  dvmptfsum  25904  ply1divex  26067  itgulm  26342  rpvmasumlem  27423  dchrmusum2  27430  dchrisum0lem2  27454  dchrisum0lem3  27455  mulog2sumlem2  27471  pntibndlem3  27528  wwlksubclwwlk  30033  blocni  30780  superpos  32329  chirredlem2  32366  eulerpartlemgvv  34384  ballotlemfc0  34501  ballotlemfcc  34502  bj-finsumval0  37318  pibt2  37450  fin2solem  37645  matunitlindflem1  37655  poimirlem28  37687  heicant  37694  ftc1anclem6  37737  ftc1anc  37740  fdc  37784  incsequz  37787  ismtyres  37847  isdrngo2  37997  rngohomco  38013  keridl  38071  linepsubN  39790  pmapsub  39806  fsuppind  42622  mhpind  42626  mzpcompact2lem  42783  pellex  42867  monotuz  42973  unxpwdom3  43127  cantnfresb  43356  dssmapnvod  44052  radcnvrat  44346  fprodexp  45633  fprodabs2  45634  climxrrelem  45786  dvnprodlem1  45983  stoweidlem34  46071  fourierdlem42  46186  elaa2  46271  sge0iunmptlemfi  46450  aacllem  49832