Theorem adantlrr 722

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 682	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  5097  2ndconst  8053  oelim  8471  odi  8516  marypha1lem  9348  dfac12lem2  10067  infunsdom  10135  isf34lem4  10299  distrlem1pr  10948  lcmgcdlem  16545  lcmdvds  16547  drsdirfi  18240  isacs3lem  18477  conjnmzb  19194  psgndif  21569  frlmsslsp  21763  metss2lem  24467  nghmcn  24701  bndth  24925  itg2monolem1  25719  dvmptfsum  25947  ply1divex  26110  itgulm  26385  rpvmasumlem  27466  dchrmusum2  27473  dchrisum0lem2  27497  dchrisum0lem3  27498  mulog2sumlem2  27514  pntibndlem3  27571  wwlksubclwwlk  30145  blocni  30892  superpos  32441  chirredlem2  32478  eulerpartlemgvv  34553  ballotlemfc0  34670  ballotlemfcc  34671  bj-finsumval0  37534  pibt2  37666  fin2solem  37851  matunitlindflem1  37861  poimirlem28  37893  heicant  37900  ftc1anclem6  37943  ftc1anc  37946  fdc  37990  incsequz  37993  ismtyres  38053  isdrngo2  38203  rngohomco  38219  keridl  38277  linepsubN  40122  pmapsub  40138  fsuppind  42942  mhpind  42946  mzpcompact2lem  43102  pellex  43186  monotuz  43292  unxpwdom3  43446  cantnfresb  43675  dssmapnvod  44370  radcnvrat  44664  fprodexp  45948  fprodabs2  45949  climxrrelem  46101  dvnprodlem1  46298  stoweidlem34  46386  fourierdlem42  46501  elaa2  46586  sge0iunmptlemfi  46765  aacllem  50154