Theorem adantrrr 738

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 488	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr2 696	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:  brab2d  5517  zorn2lem6  10609  addsrmo  11188  mulsrmo  11189  lemul12b  12204  lt2mul2div  12225  lediv12a  12240  tgcl  23320  neissex  23478  alexsublem  24396  alexsubALTlem4  24402  iscmet3  25647  mulsuniflem  28568  ablo4  31185  shscli  31952  mdslmd3i  32967  cvmliftmolem2  36227  mblfinlem4  38783  heibor  38958  ablo4pnp  39017  crngm4  39140  cvratlem  40681  ps-2  40738  cdlemftr3  41825  mzpcompact2lem  43966