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  10461  addsrmo  11033  mulsrmo  11034  lemul12b  12046  lt2mul2div  12068  lediv12a  12083  tgcl  22863  neissex  23021  alexsublem  23938  alexsubALTlem4  23944  iscmet3  25200  mulsuniflem  28059  ablo4  30486  shscli  31253  mdslmd3i  32268  brab2d  32542  cvmliftmolem2  35276  mblfinlem4  37661  heibor  37822  ablo4pnp  37881  crngm4  38004  cvratlem  39422  ps-2  39479  cdlemftr3  40566  mzpcompact2lem  42746