Theorem adantlrl 756

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  omlimcl  7703  odi  7704  oelim2  7720  mapxpen  8167  unwdomg  8530  dfac12lem2  9004  infunsdom  9074  fin1a2s  9274  frlmup1  20185  fbasrn  21735  lmmbr  23102  grporcan  27500  unoplin  28907  hmoplin  28929  superpos  29341  subfacp1lem5  31292  matunitlindflem1  33535  poimirlem4  33543  itg2addnclem  33591  ftc1anclem6  33620  fdc  33671  ismtyres  33737  isdrngo2  33887  rngohomco  33903  rngoisocnv  33910  dssmapnvod  38631  climxrrelem  40299  dvdsn1add  40472  dvnprodlem1  40479  stoweidlem27  40562  fourierdlem97  40738  qndenserrnbllem  40832  sge0iunmptlemfi  40948