Theorem adantrrr 723

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 485	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr2 681	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  zorn2lem6  9925  addsrmo  10497  mulsrmo  10498  lemul12b  11499  lt2mul2div  11520  lediv12a  11535  tgcl  21579  neissex  21737  alexsublem  22654  alexsubALTlem4  22660  iscmet3  23898  ablo4  28329  shscli  29096  mdslmd3i  30111  cvmliftmolem2  32531  mblfinlem4  34934  heibor  35101  ablo4pnp  35160  crngm4  35283  cvratlem  36559  ps-2  36616  cdlemftr3  37703  mzpcompact2lem  39355