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  5107  2ndconst  8083  oelim  8501  odi  8546  marypha1lem  9391  dfac12lem2  10105  infunsdom  10173  isf34lem4  10337  distrlem1pr  10985  lcmgcdlem  16583  lcmdvds  16585  drsdirfi  18273  isacs3lem  18508  conjnmzb  19192  psgndif  21518  frlmsslsp  21712  metss2lem  24406  nghmcn  24640  bndth  24864  itg2monolem1  25658  dvmptfsum  25886  ply1divex  26049  itgulm  26324  rpvmasumlem  27405  dchrmusum2  27412  dchrisum0lem2  27436  dchrisum0lem3  27437  mulog2sumlem2  27453  pntibndlem3  27510  wwlksubclwwlk  29994  blocni  30741  superpos  32290  chirredlem2  32327  eulerpartlemgvv  34374  ballotlemfc0  34491  ballotlemfcc  34492  bj-finsumval0  37280  pibt2  37412  fin2solem  37607  matunitlindflem1  37617  poimirlem28  37649  heicant  37656  ftc1anclem6  37699  ftc1anc  37702  fdc  37746  incsequz  37749  ismtyres  37809  isdrngo2  37959  rngohomco  37975  keridl  38033  linepsubN  39753  pmapsub  39769  fsuppind  42585  mhpind  42589  mzpcompact2lem  42746  pellex  42830  monotuz  42937  unxpwdom3  43091  cantnfresb  43320  dssmapnvod  44016  radcnvrat  44310  fprodexp  45599  fprodabs2  45600  climxrrelem  45754  dvnprodlem1  45951  stoweidlem34  46039  fourierdlem42  46154  elaa2  46239  sge0iunmptlemfi  46418  aacllem  49794