Theorem adantlrl 732

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  1stconst  8096  omlimcl  8564  odi  8565  oelim2  8582  mapxpen  9132  unwdomg  9547  dfac12lem2  10129  infunsdom  10197  fin1a2s  10399  ccatpfx  14740  frlmup1  21929  fbasrn  24022  lmmbr  25398  grporcan  30848  unoplin  32250  hmoplin  32272  superpos  32684  ccatf1  33247  subfacp1lem5  35654  matunitlindflem1  38245  poimirlem4  38253  itg2addnclem  38300  ftc1anclem6  38327  fdc  38374  ismtyres  38437  isdrngo2  38587  rngohomco  38603  rngoisocnv  38610  dssmapnvod  44726  climxrrelem  46443  dvdsn1add  46633  dvnprodlem1  46640  stoweidlem27  46721  fourierdlem97  46897  qndenserrnbllem  46988  sge0iunmptlemfi  47107