Theorem adantlrr 717

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 677	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 206  df-an 396

This theorem is referenced by:  disjxiun  5067  2ndconst  7912  oelim  8326  odi  8372  marypha1lem  9122  dfac12lem2  9831  infunsdom  9901  isf34lem4  10064  distrlem1pr  10712  lcmgcdlem  16239  lcmdvds  16241  drsdirfi  17938  isacs3lem  18175  conjnmzb  18784  psgndif  20719  frlmsslsp  20913  metss2lem  23573  nghmcn  23815  bndth  24027  itg2monolem1  24820  dvmptfsum  25044  ply1divex  25206  itgulm  25472  rpvmasumlem  26540  dchrmusum2  26547  dchrisum0lem2  26571  dchrisum0lem3  26572  mulog2sumlem2  26588  pntibndlem3  26645  wwlksubclwwlk  28323  blocni  29068  superpos  30617  chirredlem2  30654  eulerpartlemgvv  32243  ballotlemfc0  32359  ballotlemfcc  32360  bj-finsumval0  35383  pibt2  35515  fin2solem  35690  matunitlindflem1  35700  poimirlem28  35732  heicant  35739  ftc1anclem6  35782  ftc1anc  35785  fdc  35830  incsequz  35833  ismtyres  35893  isdrngo2  36043  rngohomco  36059  keridl  36117  linepsubN  37693  pmapsub  37709  fsuppind  40202  mhpind  40206  mzpcompact2lem  40489  pellex  40573  monotuz  40679  unxpwdom3  40836  dssmapnvod  41517  radcnvrat  41821  fprodexp  43025  fprodabs2  43026  climxrrelem  43180  dvnprodlem1  43377  stoweidlem34  43465  fourierdlem42  43580  elaa2  43665  sge0iunmptlemfi  43841  aacllem  46391