Theorem adantlrr 719

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 484	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 679	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  disjxiun  5094  2ndconst  8014  oelim  8440  odi  8486  marypha1lem  9295  dfac12lem2  10006  infunsdom  10076  isf34lem4  10239  distrlem1pr  10887  lcmgcdlem  16409  lcmdvds  16411  drsdirfi  18121  isacs3lem  18358  conjnmzb  18966  psgndif  20913  frlmsslsp  21109  metss2lem  23773  nghmcn  24015  bndth  24227  itg2monolem1  25021  dvmptfsum  25245  ply1divex  25407  itgulm  25673  rpvmasumlem  26741  dchrmusum2  26748  dchrisum0lem2  26772  dchrisum0lem3  26773  mulog2sumlem2  26789  pntibndlem3  26846  wwlksubclwwlk  28710  blocni  29455  superpos  31004  chirredlem2  31041  eulerpartlemgvv  32641  ballotlemfc0  32757  ballotlemfcc  32758  bj-finsumval0  35610  pibt2  35742  fin2solem  35917  matunitlindflem1  35927  poimirlem28  35959  heicant  35966  ftc1anclem6  36009  ftc1anc  36012  fdc  36057  incsequz  36060  ismtyres  36120  isdrngo2  36270  rngohomco  36286  keridl  36344  linepsubN  38069  pmapsub  38085  fsuppind  40588  mhpind  40592  mzpcompact2lem  40884  pellex  40968  monotuz  41075  unxpwdom3  41232  dssmapnvod  41999  radcnvrat  42303  fprodexp  43521  fprodabs2  43522  climxrrelem  43676  dvnprodlem1  43873  stoweidlem34  43961  fourierdlem42  44076  elaa2  44161  sge0iunmptlemfi  44338  aacllem  46921