Theorem adantlrl 707

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
adantlrl	⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrl

Step	Hyp	Ref	Expression
1		simpr 477	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl2 668	1 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  1stconst  7603  omlimcl  8005  odi  8006  oelim2  8022  mapxpen  8479  unwdomg  8843  dfac12lem2  9364  infunsdom  9434  fin1a2s  9634  frlmup1  20644  fbasrn  22196  lmmbr  23564  grporcan  28072  unoplin  29478  hmoplin  29500  superpos  29912  subfacp1lem5  32022  matunitlindflem1  34335  poimirlem4  34343  itg2addnclem  34390  ftc1anclem6  34419  fdc  34468  ismtyres  34534  isdrngo2  34684  rngohomco  34700  rngoisocnv  34707  dssmapnvod  39735  climxrrelem  41467  dvdsn1add  41660  dvnprodlem1  41667  stoweidlem27  41749  fourierdlem97  41925  qndenserrnbllem  42016  sge0iunmptlemfi  42132