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  5103  2ndconst  8139  oelim  8570  odi  8615  marypha1lem  9452  dfac12lem2  10250  infunsdom  10318  isf34lem4  10482  distrlem1pr  11137  lcmgcdlem  16810  lcmdvds  16812  drsdirfi  18508  isacs3lem  18745  conjnmzb  19496  psgndif  21938  frlmsslsp  22132  matunitlindflem1  23024  metss2lem  24860  nghmcn  25094  bndth  25309  itg2monolem1  26101  dvmptfsum  26325  ply1divex  26485  itgulm  26765  rpvmasumlem  27844  dchrmusum2  27851  dchrisum0lem2  27875  dchrisum0lem3  27876  mulog2sumlem2  27892  pntibndlem3  27949  wwlksubclwwlk  30679  blocni  31437  superpos  32986  chirredlem2  33023  eulerpartlemgvv  35078  ballotlemfc0  35195  ballotlemfcc  35196  bj-finsumval0  38398  pibt2  38532  fin2solem  38721  poimirlem28  38758  heicant  38765  ftc1anclem6  38808  ftc1anc  38811  fdc  38871  incsequz  38874  ismtyres  38934  isdrngo2  39084  rngohomco  39100  keridl  39158  linepsubN  41001  pmapsub  41017  fsuppind  43811  mhpind  43815  mzpcompact2lem  43955  pellex  44035  monotuz  44141  unxpwdom3  44290  cantnfresb  44518  dssmapnvod  45212  radcnvrat  45490  fprodexp  46811  fprodabs2  46812  climxrrelem  46964  dvnprodlem1  47161  stoweidlem34  47249  fourierdlem42  47364  elaa2  47449  sge0iunmptlemfi  47628  aacllem  51219