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  5520  zorn2lem6  10507  addsrmo  11086  mulsrmo  11087  lemul12b  12100  lt2mul2div  12121  lediv12a  12136  tgcl  23200  neissex  23358  alexsublem  24276  alexsubALTlem4  24282  iscmet3  25527  mulsuniflem  28422  ablo4  31039  shscli  31806  mdslmd3i  32821  cvmliftmolem2  35869  mblfinlem4  38417  heibor  38579  ablo4pnp  38638  crngm4  38761  cvratlem  40302  ps-2  40359  cdlemftr3  41446  mzpcompact2lem  43604