Theorem adantrrr 731

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 689	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 208  df-an 397

This theorem is referenced by:  zorn2lem6  10421  addsrmo  10994  mulsrmo  10995  lemul12b  12010  lt2mul2div  12032  lediv12a  12047  tgcl  22959  neissex  23117  alexsublem  24034  alexsubALTlem4  24040  iscmet3  25285  mulsuniflem  28166  ablo4  30646  shscli  31413  mdslmd3i  32428  brab2d  32704  cvmliftmolem2  35517  mblfinlem4  38034  heibor  38195  ablo4pnp  38254  crngm4  38377  cvratlem  39920  ps-2  39977  cdlemftr3  41064  mzpcompact2lem  43207