Theorem adantrlr 736

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantr2.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
adantrlr	⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃)

Proof of Theorem adantrlr

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr1 695	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:  smoord  8411  addsrmo  11197  mulsrmo  11198  lediv12a  12250  nrmmetd  24948  pntrmax  27948  ablo4  31209  mdslmd3i  32991  atom1d  33012  fsumiunle  33516  esumiun  34837  poimirlem28  38834  fdc  38945  incsequz  38948  crngm4  39203  ps-2  40801  aacllem  51367