Theorem adantlrr 734

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 488	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 694	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5099  2ndconst  8114  oelim  8545  odi  8590  marypha1lem  9428  dfac12lem2  10226  infunsdom  10294  isf34lem4  10458  distrlem1pr  11113  lcmgcdlem  16786  lcmdvds  16788  drsdirfi  18484  isacs3lem  18721  conjnmzb  19472  psgndif  21913  frlmsslsp  22107  matunitlindflem1  22999  metss2lem  24835  nghmcn  25069  bndth  25284  itg2monolem1  26076  dvmptfsum  26300  ply1divex  26460  itgulm  26740  rpvmasumlem  27819  dchrmusum2  27826  dchrisum0lem2  27850  dchrisum0lem3  27851  mulog2sumlem2  27867  pntibndlem3  27924  wwlksubclwwlk  30654  blocni  31412  superpos  32961  chirredlem2  32998  eulerpartlemgvv  35054  ballotlemfc0  35171  ballotlemfcc  35172  bj-finsumval0  38299  pibt2  38433  fin2solem  38622  poimirlem28  38659  heicant  38666  ftc1anclem6  38709  ftc1anc  38712  fdc  38772  incsequz  38775  ismtyres  38835  isdrngo2  38985  rngohomco  39001  keridl  39059  linepsubN  40902  pmapsub  40918  fsuppind  43711  mhpind  43715  mzpcompact2lem  43855  pellex  43935  monotuz  44041  unxpwdom3  44190  cantnfresb  44419  dssmapnvod  45113  radcnvrat  45391  fprodexp  46699  fprodabs2  46700  climxrrelem  46852  dvnprodlem1  47049  stoweidlem34  47137  fourierdlem42  47252  elaa2  47337  sge0iunmptlemfi  47516  aacllem  51107