Theorem adantlrr 721

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  disjxiun  5036  2ndconst  7847  oelim  8239  odi  8285  marypha1lem  9027  dfac12lem2  9723  infunsdom  9793  isf34lem4  9956  distrlem1pr  10604  lcmgcdlem  16126  lcmdvds  16128  drsdirfi  17766  isacs3lem  18002  conjnmzb  18611  psgndif  20518  frlmsslsp  20712  metss2lem  23363  nghmcn  23597  bndth  23809  itg2monolem1  24602  dvmptfsum  24826  ply1divex  24988  itgulm  25254  rpvmasumlem  26322  dchrmusum2  26329  dchrisum0lem2  26353  dchrisum0lem3  26354  mulog2sumlem2  26370  pntibndlem3  26427  wwlksubclwwlk  28095  blocni  28840  superpos  30389  chirredlem2  30426  eulerpartlemgvv  32009  ballotlemfc0  32125  ballotlemfcc  32126  bj-finsumval0  35140  pibt2  35274  fin2solem  35449  matunitlindflem1  35459  poimirlem28  35491  heicant  35498  ftc1anclem6  35541  ftc1anc  35544  fdc  35589  incsequz  35592  ismtyres  35652  isdrngo2  35802  rngohomco  35818  keridl  35876  linepsubN  37452  pmapsub  37468  fsuppind  39930  mhpind  39934  mzpcompact2lem  40217  pellex  40301  monotuz  40407  unxpwdom3  40564  dssmapnvod  41246  radcnvrat  41546  fprodexp  42753  fprodabs2  42754  climxrrelem  42908  dvnprodlem1  43105  stoweidlem34  43193  fourierdlem42  43308  elaa2  43393  sge0iunmptlemfi  43569  aacllem  46119