Theorem adantlrr 727

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  disjxiun  5076  2ndconst  8047  oelim  8466  odi  8511  marypha1lem  9343  dfac12lem2  10065  infunsdom  10133  isf34lem4  10297  distrlem1pr  10946  lcmgcdlem  16573  lcmdvds  16575  drsdirfi  18269  isacs3lem  18506  conjnmzb  19226  psgndif  21584  frlmsslsp  21778  metss2lem  24501  nghmcn  24735  bndth  24950  itg2monolem1  25742  dvmptfsum  25967  ply1divex  26127  itgulm  26398  rpvmasumlem  27475  dchrmusum2  27482  dchrisum0lem2  27506  dchrisum0lem3  27507  mulog2sumlem2  27523  pntibndlem3  27580  wwlksubclwwlk  30153  blocni  30901  superpos  32450  chirredlem2  32487  eulerpartlemgvv  34567  ballotlemfc0  34684  ballotlemfcc  34685  bj-finsumval0  37652  pibt2  37786  fin2solem  37980  matunitlindflem1  37990  poimirlem28  38022  heicant  38029  ftc1anclem6  38072  ftc1anc  38075  fdc  38119  incsequz  38122  ismtyres  38182  isdrngo2  38332  rngohomco  38348  keridl  38406  linepsubN  40251  pmapsub  40267  fsuppind  43047  mhpind  43051  mzpcompact2lem  43207  pellex  43287  monotuz  43393  unxpwdom3  43547  cantnfresb  43776  dssmapnvod  44471  radcnvrat  44765  fprodexp  46046  fprodabs2  46047  climxrrelem  46199  dvnprodlem1  46396  stoweidlem34  46484  fourierdlem42  46599  elaa2  46684  sge0iunmptlemfi  46863  aacllem  50298