Theorem adantrrr 724

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 682	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  10570  addsrmo  11142  mulsrmo  11143  lemul12b  12151  lt2mul2div  12173  lediv12a  12188  tgcl  22997  neissex  23156  alexsublem  24073  alexsubALTlem4  24079  iscmet3  25346  mulsuniflem  28193  ablo4  30582  shscli  31349  mdslmd3i  32364  brab2d  32629  cvmliftmolem2  35250  mblfinlem4  37620  heibor  37781  ablo4pnp  37840  crngm4  37963  cvratlem  39378  ps-2  39435  cdlemftr3  40522  mzpcompact2lem  42707