Theorem adantrrr 722

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 680	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  10350  addsrmo  10922  mulsrmo  10923  lemul12b  11925  lt2mul2div  11946  lediv12a  11961  tgcl  22217  neissex  22376  alexsublem  23293  alexsubALTlem4  23299  iscmet3  24555  ablo4  29113  shscli  29880  mdslmd3i  30895  cvmliftmolem2  33456  mblfinlem4  35915  heibor  36077  ablo4pnp  36136  crngm4  36259  cvratlem  37682  ps-2  37739  cdlemftr3  38826  mzpcompact2lem  40823