Theorem adantlrl 733

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 490	. 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:  1stconst  8104  omlimcl  8572  odi  8573  oelim2  8590  mapxpen  9141  unwdomg  9556  dfac12lem2  10147  infunsdom  10215  fin1a2s  10416  ccatf1  14648  ccatpfx  14762  frlmup1  21985  fbasrn  24078  lmmbr  25454  grporcan  30907  unoplin  32309  hmoplin  32331  superpos  32743  subfacp1lem5  35697  matunitlindflem1  38308  poimirlem4  38316  itg2addnclem  38363  ftc1anclem6  38390  fdc  38437  ismtyres  38500  isdrngo2  38650  rngohomco  38666  rngoisocnv  38673  dssmapnvod  44787  climxrrelem  46504  dvdsn1add  46694  dvnprodlem1  46701  stoweidlem27  46782  fourierdlem97  46958  qndenserrnbllem  47049  sge0iunmptlemfi  47168