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  10498  addsrmo  11070  mulsrmo  11071  lemul12b  12073  lt2mul2div  12094  lediv12a  12109  tgcl  22479  neissex  22638  alexsublem  23555  alexsubALTlem4  23561  iscmet3  24817  mulsuniflem  27614  ablo4  29841  shscli  30608  mdslmd3i  31623  cvmliftmolem2  34342  mblfinlem4  36614  heibor  36775  ablo4pnp  36834  crngm4  36957  cvratlem  38378  ps-2  38435  cdlemftr3  39522  mzpcompact2lem  41571