Theorem adantlrr 720

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 680	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  5163  2ndconst  8142  oelim  8590  odi  8635  marypha1lem  9502  dfac12lem2  10214  infunsdom  10282  isf34lem4  10446  distrlem1pr  11094  lcmgcdlem  16653  lcmdvds  16655  drsdirfi  18375  isacs3lem  18612  conjnmzb  19293  psgndif  21643  frlmsslsp  21839  metss2lem  24545  nghmcn  24787  bndth  25009  itg2monolem1  25805  dvmptfsum  26033  ply1divex  26196  itgulm  26469  rpvmasumlem  27549  dchrmusum2  27556  dchrisum0lem2  27580  dchrisum0lem3  27581  mulog2sumlem2  27597  pntibndlem3  27654  wwlksubclwwlk  30090  blocni  30837  superpos  32386  chirredlem2  32423  eulerpartlemgvv  34341  ballotlemfc0  34457  ballotlemfcc  34458  bj-finsumval0  37251  pibt2  37383  fin2solem  37566  matunitlindflem1  37576  poimirlem28  37608  heicant  37615  ftc1anclem6  37658  ftc1anc  37661  fdc  37705  incsequz  37708  ismtyres  37768  isdrngo2  37918  rngohomco  37934  keridl  37992  linepsubN  39709  pmapsub  39725  fsuppind  42545  mhpind  42549  mzpcompact2lem  42707  pellex  42791  monotuz  42898  unxpwdom3  43052  cantnfresb  43286  dssmapnvod  43982  radcnvrat  44283  fprodexp  45515  fprodabs2  45516  climxrrelem  45670  dvnprodlem1  45867  stoweidlem34  45955  fourierdlem42  46070  elaa2  46155  sge0iunmptlemfi  46334  aacllem  48895