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  8100  omlimcl  8570  odi  8571  oelim2  8588  mapxpen  9146  unwdomg  9562  dfac12lem2  10204  infunsdom  10272  fin1a2s  10473  ccatf1  14716  ccatpfx  14830  frlmup1  22084  matunitlindflem1  22974  fbasrn  24183  lmmbr  25559  grporcan  31102  unoplin  32504  hmoplin  32526  superpos  32938  subfacp1lem5  35918  poimirlem4  38510  itg2addnclem  38557  ftc1anclem6  38584  fdc  38647  ismtyres  38710  isdrngo2  38860  rngohomco  38876  rngoisocnv  38883  dssmapnvod  44979  climxrrelem  46703  dvdsn1add  46893  dvnprodlem1  46900  stoweidlem27  46981  fourierdlem97  47157  qndenserrnbllem  47248  sge0iunmptlemfi  47367