Theorem adantlrl 720

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  1stconst  8033  omlimcl  8496  odi  8497  oelim2  8513  mapxpen  9060  unwdomg  9476  dfac12lem2  10039  infunsdom  10107  fin1a2s  10308  ccatpfx  14607  frlmup1  21705  fbasrn  23769  lmmbr  25156  grporcan  30462  unoplin  31864  hmoplin  31886  superpos  32298  ccatf1  32890  subfacp1lem5  35157  matunitlindflem1  37596  poimirlem4  37604  itg2addnclem  37651  ftc1anclem6  37678  fdc  37725  ismtyres  37788  isdrngo2  37938  rngohomco  37954  rngoisocnv  37961  dssmapnvod  43993  climxrrelem  45730  dvdsn1add  45920  dvnprodlem1  45927  stoweidlem27  46008  fourierdlem97  46184  qndenserrnbllem  46275  sge0iunmptlemfi  46394