Theorem adantrrr 722

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 680	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 206  df-an 397

This theorem is referenced by:  zorn2lem6  10257  addsrmo  10829  mulsrmo  10830  lemul12b  11832  lt2mul2div  11853  lediv12a  11868  tgcl  22119  neissex  22278  alexsublem  23195  alexsubALTlem4  23201  iscmet3  24457  ablo4  28912  shscli  29679  mdslmd3i  30694  cvmliftmolem2  33244  mblfinlem4  35817  heibor  35979  ablo4pnp  36038  crngm4  36161  cvratlem  37435  ps-2  37492  cdlemftr3  38579  mzpcompact2lem  40573