Theorem adantlrr 722

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 682	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  5082  2ndconst  8051  oelim  8469  odi  8514  marypha1lem  9346  dfac12lem2  10067  infunsdom  10135  isf34lem4  10299  distrlem1pr  10948  lcmgcdlem  16575  lcmdvds  16577  drsdirfi  18271  isacs3lem  18508  conjnmzb  19228  psgndif  21582  frlmsslsp  21776  metss2lem  24476  nghmcn  24710  bndth  24925  itg2monolem1  25717  dvmptfsum  25942  ply1divex  26102  itgulm  26373  rpvmasumlem  27450  dchrmusum2  27457  dchrisum0lem2  27481  dchrisum0lem3  27482  mulog2sumlem2  27498  pntibndlem3  27555  wwlksubclwwlk  30128  blocni  30876  superpos  32425  chirredlem2  32462  eulerpartlemgvv  34520  ballotlemfc0  34637  ballotlemfcc  34638  bj-finsumval0  37599  pibt2  37733  fin2solem  37927  matunitlindflem1  37937  poimirlem28  37969  heicant  37976  ftc1anclem6  38019  ftc1anc  38022  fdc  38066  incsequz  38069  ismtyres  38129  isdrngo2  38279  rngohomco  38295  keridl  38353  linepsubN  40198  pmapsub  40214  fsuppind  43023  mhpind  43027  mzpcompact2lem  43183  pellex  43263  monotuz  43369  unxpwdom3  43523  cantnfresb  43752  dssmapnvod  44447  radcnvrat  44741  fprodexp  46024  fprodabs2  46025  climxrrelem  46177  dvnprodlem1  46374  stoweidlem34  46462  fourierdlem42  46577  elaa2  46662  sge0iunmptlemfi  46841  aacllem  50276