Theorem adantrrr 725

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 482	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr2 683	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  zorn2lem6  10411  addsrmo  10984  mulsrmo  10985  lemul12b  11998  lt2mul2div  12020  lediv12a  12035  tgcl  22913  neissex  23071  alexsublem  23988  alexsubALTlem4  23994  iscmet3  25249  mulsuniflem  28145  ablo4  30625  shscli  31392  mdslmd3i  32407  brab2d  32683  cvmliftmolem2  35476  mblfinlem4  37857  heibor  38018  ablo4pnp  38077  crngm4  38200  cvratlem  39677  ps-2  39734  cdlemftr3  40821  mzpcompact2lem  42989