Theorem adantlrl 716

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 677	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 206  df-an 396

This theorem is referenced by:  1stconst  7911  omlimcl  8371  odi  8372  oelim2  8388  mapxpen  8879  unwdomg  9273  dfac12lem2  9831  infunsdom  9901  fin1a2s  10101  ccatpfx  14342  frlmup1  20915  fbasrn  22943  lmmbr  24327  grporcan  28781  unoplin  30183  hmoplin  30205  superpos  30617  ccatf1  31125  subfacp1lem5  33046  matunitlindflem1  35700  poimirlem4  35708  itg2addnclem  35755  ftc1anclem6  35782  fdc  35830  ismtyres  35893  isdrngo2  36043  rngohomco  36059  rngoisocnv  36066  dssmapnvod  41517  climxrrelem  43180  dvdsn1add  43370  dvnprodlem1  43377  stoweidlem27  43458  fourierdlem97  43634  qndenserrnbllem  43725  sge0iunmptlemfi  43841