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  8113  omlimcl  8589  odi  8590  oelim2  8607  mapxpen  9165  unwdomg  9581  dfac12lem2  10226  infunsdom  10294  fin1a2s  10495  ccatf1  14739  ccatpfx  14854  frlmup1  22109  matunitlindflem1  22999  fbasrn  24208  lmmbr  25584  grporcan  31125  unoplin  32527  hmoplin  32549  superpos  32961  subfacp1lem5  36035  poimirlem4  38635  itg2addnclem  38682  ftc1anclem6  38709  fdc  38772  ismtyres  38835  isdrngo2  38985  rngohomco  39001  rngoisocnv  39008  dssmapnvod  45113  climxrrelem  46852  dvdsn1add  47042  dvnprodlem1  47049  stoweidlem27  47130  fourierdlem97  47306  qndenserrnbllem  47397  sge0iunmptlemfi  47516