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  5111  2ndconst  8105  oelim  8528  odi  8573  marypha1lem  9403  dfac12lem2  10147  infunsdom  10215  isf34lem4  10379  distrlem1pr  11028  lcmgcdlem  16689  lcmdvds  16691  drsdirfi  18386  isacs3lem  18623  conjnmzb  19354  psgndif  21789  frlmsslsp  21983  metss2lem  24705  nghmcn  24939  bndth  25154  itg2monolem1  25946  dvmptfsum  26171  ply1divex  26331  itgulm  26608  rpvmasumlem  27688  dchrmusum2  27695  dchrisum0lem2  27719  dchrisum0lem3  27720  mulog2sumlem2  27736  pntibndlem3  27793  wwlksubclwwlk  30446  blocni  31194  superpos  32743  chirredlem2  32780  eulerpartlemgvv  34798  ballotlemfc0  34915  ballotlemfcc  34916  bj-finsumval0  37970  pibt2  38104  fin2solem  38298  matunitlindflem1  38308  poimirlem28  38340  heicant  38347  ftc1anclem6  38390  ftc1anc  38393  fdc  38437  incsequz  38440  ismtyres  38500  isdrngo2  38650  rngohomco  38666  keridl  38724  linepsubN  40567  pmapsub  40583  fsuppind  43363  mhpind  43367  mzpcompact2lem  43523  pellex  43603  monotuz  43709  unxpwdom3  43863  cantnfresb  44092  dssmapnvod  44787  radcnvrat  45065  fprodexp  46351  fprodabs2  46352  climxrrelem  46504  dvnprodlem1  46701  stoweidlem34  46789  fourierdlem42  46904  elaa2  46989  sge0iunmptlemfi  47168  aacllem  50662