Theorem adantrlr 761

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 474	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr1 687	1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  smoord  7632  addsrmo  10106  mulsrmo  10107  lediv12a  11128  nrmmetd  22600  pntrmax  25473  ablo4  27734  mdslmd3i  29521  atom1d  29542  fsumiunle  29905  esumiun  30486  poimirlem28  33768  fdc  33872  incsequz  33875  crngm4  34133  ps-2  35285  aacllem  43078