Theorem adantrrr 721

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

Proof of Theorem adantrrr

Step	Hyp	Ref	Expression
1		simpl 483	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr2 679	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  zorn2lem6  9758  addsrmo  10330  mulsrmo  10331  lemul12b  11334  lt2mul2div  11355  lediv12a  11370  tgcl  21249  neissex  21407  alexsublem  22324  alexsubALTlem4  22330  iscmet3  23567  ablo4  28006  shscli  28773  mdslmd3i  29788  cvmliftmolem2  32093  mblfinlem4  34409  heibor  34577  ablo4pnp  34636  crngm4  34759  cvratlem  36038  ps-2  36095  cdlemftr3  37182  mzpcompact2lem  38783