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  10423  addsrmo  10996  mulsrmo  10997  lemul12b  12012  lt2mul2div  12034  lediv12a  12049  tgcl  22934  neissex  23092  alexsublem  24009  alexsubALTlem4  24015  iscmet3  25260  mulsuniflem  28141  ablo4  30621  shscli  31388  mdslmd3i  32403  brab2d  32678  cvmliftmolem2  35464  mblfinlem4  37981  heibor  38142  ablo4pnp  38201  crngm4  38324  cvratlem  39867  ps-2  39924  cdlemftr3  41011  mzpcompact2lem  43183