Theorem adantlrr 719

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 679	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  5146  2ndconst  8106  oelim  8555  odi  8600  marypha1lem  9458  dfac12lem2  10169  infunsdom  10239  isf34lem4  10402  distrlem1pr  11050  lcmgcdlem  16580  lcmdvds  16582  drsdirfi  18300  isacs3lem  18537  conjnmzb  19216  psgndif  21551  frlmsslsp  21747  metss2lem  24464  nghmcn  24706  bndth  24928  itg2monolem1  25724  dvmptfsum  25951  ply1divex  26117  itgulm  26389  rpvmasumlem  27465  dchrmusum2  27472  dchrisum0lem2  27496  dchrisum0lem3  27497  mulog2sumlem2  27513  pntibndlem3  27570  wwlksubclwwlk  29940  blocni  30687  superpos  32236  chirredlem2  32273  eulerpartlemgvv  34127  ballotlemfc0  34243  ballotlemfcc  34244  bj-finsumval0  36895  pibt2  37027  fin2solem  37210  matunitlindflem1  37220  poimirlem28  37252  heicant  37259  ftc1anclem6  37302  ftc1anc  37305  fdc  37349  incsequz  37352  ismtyres  37412  isdrngo2  37562  rngohomco  37578  keridl  37636  linepsubN  39355  pmapsub  39371  fsuppind  41958  mhpind  41962  mzpcompact2lem  42313  pellex  42397  monotuz  42504  unxpwdom3  42661  cantnfresb  42895  dssmapnvod  43592  radcnvrat  43893  fprodexp  45120  fprodabs2  45121  climxrrelem  45275  dvnprodlem1  45472  stoweidlem34  45560  fourierdlem42  45675  elaa2  45760  sge0iunmptlemfi  45939  aacllem  48420