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  10541  addsrmo  11113  mulsrmo  11114  lemul12b  12124  lt2mul2div  12146  lediv12a  12161  tgcl  22976  neissex  23135  alexsublem  24052  alexsubALTlem4  24058  iscmet3  25327  mulsuniflem  28175  ablo4  30569  shscli  31336  mdslmd3i  32351  brab2d  32619  cvmliftmolem2  35287  mblfinlem4  37667  heibor  37828  ablo4pnp  37887  crngm4  38010  cvratlem  39423  ps-2  39480  cdlemftr3  40567  mzpcompact2lem  42762