Theorem adantlrr 733

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5107  2ndconst  8097  oelim  8520  odi  8565  marypha1lem  9394  dfac12lem2  10129  infunsdom  10197  isf34lem4  10362  distrlem1pr  11011  lcmgcdlem  16665  lcmdvds  16667  drsdirfi  18362  isacs3lem  18599  conjnmzb  19324  psgndif  21733  frlmsslsp  21927  metss2lem  24649  nghmcn  24883  bndth  25098  itg2monolem1  25890  dvmptfsum  26115  ply1divex  26275  itgulm  26549  rpvmasumlem  27629  dchrmusum2  27636  dchrisum0lem2  27660  dchrisum0lem3  27661  mulog2sumlem2  27677  pntibndlem3  27734  wwlksubclwwlk  30387  blocni  31135  superpos  32684  chirredlem2  32721  eulerpartlemgvv  34744  ballotlemfc0  34861  ballotlemfcc  34862  bj-finsumval0  37907  pibt2  38041  fin2solem  38235  matunitlindflem1  38245  poimirlem28  38277  heicant  38284  ftc1anclem6  38327  ftc1anc  38330  fdc  38374  incsequz  38377  ismtyres  38437  isdrngo2  38587  rngohomco  38603  keridl  38661  linepsubN  40504  pmapsub  40520  fsuppind  43302  mhpind  43306  mzpcompact2lem  43462  pellex  43542  monotuz  43648  unxpwdom3  43802  cantnfresb  44031  dssmapnvod  44726  radcnvrat  45004  fprodexp  46290  fprodabs2  46291  climxrrelem  46443  dvnprodlem1  46640  stoweidlem34  46728  fourierdlem42  46843  elaa2  46928  sge0iunmptlemfi  47107  aacllem  50578