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  8138  omlimcl  8614  odi  8615  oelim2  8632  mapxpen  9190  unwdomg  9605  dfac12lem2  10250  infunsdom  10318  fin1a2s  10519  ccatf1  14763  ccatpfx  14878  frlmup1  22134  matunitlindflem1  23024  fbasrn  24233  lmmbr  25609  grporcan  31150  unoplin  32552  hmoplin  32574  superpos  32986  subfacp1lem5  36116  poimirlem4  38734  itg2addnclem  38781  ftc1anclem6  38808  fdc  38871  ismtyres  38934  isdrngo2  39084  rngohomco  39100  rngoisocnv  39107  dssmapnvod  45212  climxrrelem  46964  dvdsn1add  47154  dvnprodlem1  47161  stoweidlem27  47242  fourierdlem97  47418  qndenserrnbllem  47509  sge0iunmptlemfi  47628