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 483	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr2 681	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  10446  addsrmo  11018  mulsrmo  11019  lemul12b  12021  lt2mul2div  12042  lediv12a  12057  tgcl  22356  neissex  22515  alexsublem  23432  alexsubALTlem4  23438  iscmet3  24694  ablo4  29555  shscli  30322  mdslmd3i  31337  cvmliftmolem2  33963  mblfinlem4  36191  heibor  36353  ablo4pnp  36412  crngm4  36535  cvratlem  37957  ps-2  38014  cdlemftr3  39101  mzpcompact2lem  41132