Theorem adantrrr 726

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 684	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  10414  addsrmo  10987  mulsrmo  10988  lemul12b  12003  lt2mul2div  12025  lediv12a  12040  tgcl  22944  neissex  23102  alexsublem  24019  alexsubALTlem4  24025  iscmet3  25270  mulsuniflem  28155  ablo4  30636  shscli  31403  mdslmd3i  32418  brab2d  32693  cvmliftmolem2  35480  mblfinlem4  37995  heibor  38156  ablo4pnp  38215  crngm4  38338  cvratlem  39881  ps-2  39938  cdlemftr3  41025  mzpcompact2lem  43197