Theorem adantlrr 734

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5100  2ndconst  8101  oelim  8526  odi  8571  marypha1lem  9409  dfac12lem2  10204  infunsdom  10272  isf34lem4  10436  distrlem1pr  11091  lcmgcdlem  16761  lcmdvds  16763  drsdirfi  18459  isacs3lem  18696  conjnmzb  19447  psgndif  21888  frlmsslsp  22082  matunitlindflem1  22974  metss2lem  24810  nghmcn  25044  bndth  25259  itg2monolem1  26051  dvmptfsum  26275  ply1divex  26435  itgulm  26717  rpvmasumlem  27796  dchrmusum2  27803  dchrisum0lem2  27827  dchrisum0lem3  27828  mulog2sumlem2  27844  pntibndlem3  27901  wwlksubclwwlk  30631  blocni  31389  superpos  32938  chirredlem2  32975  eulerpartlemgvv  34991  ballotlemfc0  35108  ballotlemfcc  35109  bj-finsumval0  38174  pibt2  38308  fin2solem  38497  poimirlem28  38534  heicant  38541  ftc1anclem6  38584  ftc1anc  38587  fdc  38647  incsequz  38650  ismtyres  38710  isdrngo2  38860  rngohomco  38876  keridl  38934  linepsubN  40777  pmapsub  40793  fsuppind  43580  mhpind  43584  mzpcompact2lem  43715  pellex  43795  monotuz  43901  unxpwdom3  44055  cantnfresb  44284  dssmapnvod  44979  radcnvrat  45257  fprodexp  46550  fprodabs2  46551  climxrrelem  46703  dvnprodlem1  46900  stoweidlem34  46988  fourierdlem42  47103  elaa2  47188  sge0iunmptlemfi  47367  aacllem  50883