Theorem adantrrr 737

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  brab2d  5513  zorn2lem6  10473  addsrmo  11046  mulsrmo  11047  lemul12b  12063  lt2mul2div  12084  lediv12a  12099  tgcl  23087  neissex  23245  alexsublem  24162  alexsubALTlem4  24168  iscmet3  25413  mulsuniflem  28300  ablo4  30811  shscli  31578  mdslmd3i  32593  cvmliftmolem2  35645  mblfinlem4  38171  heibor  38332  ablo4pnp  38391  crngm4  38514  cvratlem  40057  ps-2  40114  cdlemftr3  41201  mzpcompact2lem  43344