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 ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

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 401

This theorem is used by:  1stconst  8093  omlimcl  8561  odi  8562  oelim2  8579  mapxpen  9129  unwdomg  9544  dfac12lem2  10135  infunsdom  10203  fin1a2s  10404  ccatpfx  14745  frlmup1  21959  fbasrn  24052  lmmbr  25428  grporcan  30881  unoplin  32283  hmoplin  32305  superpos  32717  ccatf1  33278  subfacp1lem5  35684  matunitlindflem1  38295  poimirlem4  38303  itg2addnclem  38350  ftc1anclem6  38377  fdc  38424  ismtyres  38487  isdrngo2  38637  rngohomco  38653  rngoisocnv  38660  dssmapnvod  44774  climxrrelem  46491  dvdsn1add  46681  dvnprodlem1  46688  stoweidlem27  46769  fourierdlem97  46945  qndenserrnbllem  47036  sge0iunmptlemfi  47155