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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  zorn2lem6  10498  addsrmo  11070  mulsrmo  11071  lemul12b  12075  lt2mul2div  12096  lediv12a  12111  tgcl  22692  neissex  22851  alexsublem  23768  alexsubALTlem4  23774  iscmet3  25034  mulsuniflem  27831  ablo4  30058  shscli  30825  mdslmd3i  31840  cvmliftmolem2  34559  mblfinlem4  36831  heibor  36992  ablo4pnp  37051  crngm4  37174  cvratlem  38595  ps-2  38652  cdlemftr3  39739  mzpcompact2lem  41791