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  10399  addsrmo  10971  mulsrmo  10972  lemul12b  11985  lt2mul2div  12007  lediv12a  12022  tgcl  22885  neissex  23043  alexsublem  23960  alexsubALTlem4  23966  iscmet3  25221  mulsuniflem  28089  ablo4  30532  shscli  31299  mdslmd3i  32314  brab2d  32590  cvmliftmolem2  35347  mblfinlem4  37720  heibor  37881  ablo4pnp  37940  crngm4  38063  cvratlem  39540  ps-2  39597  cdlemftr3  40684  mzpcompact2lem  42868