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

This theorem is referenced by:  disjxiun  5144  2ndconst  8083  oelim  8530  odi  8575  marypha1lem  9424  dfac12lem2  10135  infunsdom  10205  isf34lem4  10368  distrlem1pr  11016  lcmgcdlem  16539  lcmdvds  16541  drsdirfi  18254  isacs3lem  18491  conjnmzb  19121  psgndif  21146  frlmsslsp  21342  metss2lem  24011  nghmcn  24253  bndth  24465  itg2monolem1  25259  dvmptfsum  25483  ply1divex  25645  itgulm  25911  rpvmasumlem  26979  dchrmusum2  26986  dchrisum0lem2  27010  dchrisum0lem3  27011  mulog2sumlem2  27027  pntibndlem3  27084  wwlksubclwwlk  29300  blocni  30045  superpos  31594  chirredlem2  31631  eulerpartlemgvv  33363  ballotlemfc0  33479  ballotlemfcc  33480  bj-finsumval0  36154  pibt2  36286  fin2solem  36462  matunitlindflem1  36472  poimirlem28  36504  heicant  36511  ftc1anclem6  36554  ftc1anc  36557  fdc  36601  incsequz  36604  ismtyres  36664  isdrngo2  36814  rngohomco  36830  keridl  36888  linepsubN  38611  pmapsub  38627  fsuppind  41159  mhpind  41163  mzpcompact2lem  41474  pellex  41558  monotuz  41665  unxpwdom3  41822  cantnfresb  42059  dssmapnvod  42756  radcnvrat  43058  fprodexp  44296  fprodabs2  44297  climxrrelem  44451  dvnprodlem1  44648  stoweidlem34  44736  fourierdlem42  44851  elaa2  44936  sge0iunmptlemfi  45115  aacllem  47801