Theorem adantlrl 718

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  1stconst  7797  omlimcl  8206  odi  8207  oelim2  8223  mapxpen  8685  unwdomg  9050  dfac12lem2  9572  infunsdom  9638  fin1a2s  9838  ccatpfx  14065  frlmup1  20944  fbasrn  22494  lmmbr  23863  grporcan  28297  unoplin  29699  hmoplin  29721  superpos  30133  ccatf1  30627  subfacp1lem5  32433  matunitlindflem1  34890  poimirlem4  34898  itg2addnclem  34945  ftc1anclem6  34974  fdc  35022  ismtyres  35088  isdrngo2  35238  rngohomco  35254  rngoisocnv  35261  dssmapnvod  40373  climxrrelem  42037  dvdsn1add  42231  dvnprodlem1  42238  stoweidlem27  42319  fourierdlem97  42495  qndenserrnbllem  42586  sge0iunmptlemfi  42702