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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  disjxiun  5144  2ndconst  8089  oelim  8536  odi  8581  marypha1lem  9430  dfac12lem2  10141  infunsdom  10211  isf34lem4  10374  distrlem1pr  11022  lcmgcdlem  16547  lcmdvds  16549  drsdirfi  18262  isacs3lem  18499  conjnmzb  19167  psgndif  21374  frlmsslsp  21570  metss2lem  24240  nghmcn  24482  bndth  24704  itg2monolem1  25500  dvmptfsum  25727  ply1divex  25889  itgulm  26156  rpvmasumlem  27226  dchrmusum2  27233  dchrisum0lem2  27257  dchrisum0lem3  27258  mulog2sumlem2  27274  pntibndlem3  27331  wwlksubclwwlk  29578  blocni  30325  superpos  31874  chirredlem2  31911  eulerpartlemgvv  33673  ballotlemfc0  33789  ballotlemfcc  33790  bj-finsumval0  36469  pibt2  36601  fin2solem  36777  matunitlindflem1  36787  poimirlem28  36819  heicant  36826  ftc1anclem6  36869  ftc1anc  36872  fdc  36916  incsequz  36919  ismtyres  36979  isdrngo2  37129  rngohomco  37145  keridl  37203  linepsubN  38926  pmapsub  38942  fsuppind  41464  mhpind  41468  mzpcompact2lem  41791  pellex  41875  monotuz  41982  unxpwdom3  42139  cantnfresb  42376  dssmapnvod  43073  radcnvrat  43375  fprodexp  44608  fprodabs2  44609  climxrrelem  44763  dvnprodlem1  44960  stoweidlem34  45048  fourierdlem42  45163  elaa2  45248  sge0iunmptlemfi  45427  aacllem  47935