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  5512  zorn2lem6  10560  addsrmo  11139  mulsrmo  11140  lemul12b  12155  lt2mul2div  12176  lediv12a  12191  tgcl  23267  neissex  23425  alexsublem  24343  alexsubALTlem4  24349  iscmet3  25594  mulsuniflem  28517  ablo4  31134  shscli  31901  mdslmd3i  32916  cvmliftmolem2  36016  mblfinlem4  38546  heibor  38723  ablo4pnp  38782  crngm4  38905  cvratlem  40446  ps-2  40503  cdlemftr3  41590  mzpcompact2lem  43715