Theorem adantlrr 721

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 681	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  5139  2ndconst  8127  oelim  8573  odi  8618  marypha1lem  9474  dfac12lem2  10186  infunsdom  10254  isf34lem4  10418  distrlem1pr  11066  lcmgcdlem  16644  lcmdvds  16646  drsdirfi  18352  isacs3lem  18588  conjnmzb  19272  psgndif  21621  frlmsslsp  21817  metss2lem  24525  nghmcn  24767  bndth  24991  itg2monolem1  25786  dvmptfsum  26014  ply1divex  26177  itgulm  26452  rpvmasumlem  27532  dchrmusum2  27539  dchrisum0lem2  27563  dchrisum0lem3  27564  mulog2sumlem2  27580  pntibndlem3  27637  wwlksubclwwlk  30078  blocni  30825  superpos  32374  chirredlem2  32411  eulerpartlemgvv  34379  ballotlemfc0  34496  ballotlemfcc  34497  bj-finsumval0  37287  pibt2  37419  fin2solem  37614  matunitlindflem1  37624  poimirlem28  37656  heicant  37663  ftc1anclem6  37706  ftc1anc  37709  fdc  37753  incsequz  37756  ismtyres  37816  isdrngo2  37966  rngohomco  37982  keridl  38040  linepsubN  39755  pmapsub  39771  fsuppind  42605  mhpind  42609  mzpcompact2lem  42767  pellex  42851  monotuz  42958  unxpwdom3  43112  cantnfresb  43342  dssmapnvod  44038  radcnvrat  44338  fprodexp  45614  fprodabs2  45615  climxrrelem  45769  dvnprodlem1  45966  stoweidlem34  46054  fourierdlem42  46169  elaa2  46254  sge0iunmptlemfi  46433  aacllem  49375