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  10515  addsrmo  11087  mulsrmo  11088  lemul12b  12098  lt2mul2div  12120  lediv12a  12135  tgcl  22907  neissex  23065  alexsublem  23982  alexsubALTlem4  23988  iscmet3  25245  mulsuniflem  28104  ablo4  30531  shscli  31298  mdslmd3i  32313  brab2d  32587  cvmliftmolem2  35304  mblfinlem4  37684  heibor  37845  ablo4pnp  37904  crngm4  38027  cvratlem  39440  ps-2  39497  cdlemftr3  40584  mzpcompact2lem  42774