Theorem adantrrr 723

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  zorn2lem6  9923  addsrmo  10495  mulsrmo  10496  lemul12b  11497  lt2mul2div  11518  lediv12a  11533  tgcl  21577  neissex  21735  alexsublem  22652  alexsubALTlem4  22658  iscmet3  23896  ablo4  28327  shscli  29094  mdslmd3i  30109  cvmliftmolem2  32529  mblfinlem4  34947  heibor  35114  ablo4pnp  35173  crngm4  35296  cvratlem  36572  ps-2  36629  cdlemftr3  37716  mzpcompact2lem  39368