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  8030  omlimcl  8493  odi  8494  oelim2  8510  mapxpen  9056  unwdomg  9470  dfac12lem2  10033  infunsdom  10101  fin1a2s  10302  ccatpfx  14605  frlmup1  21733  fbasrn  23797  lmmbr  25183  grporcan  30493  unoplin  31895  hmoplin  31917  superpos  32329  ccatf1  32925  subfacp1lem5  35216  matunitlindflem1  37655  poimirlem4  37663  itg2addnclem  37710  ftc1anclem6  37737  fdc  37784  ismtyres  37847  isdrngo2  37997  rngohomco  38013  rngoisocnv  38020  dssmapnvod  44052  climxrrelem  45786  dvdsn1add  45976  dvnprodlem1  45983  stoweidlem27  46064  fourierdlem97  46240  qndenserrnbllem  46331  sge0iunmptlemfi  46450