Theorem adantrrr 738

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  brab2d  5511  zorn2lem6  10582  addsrmo  11161  mulsrmo  11162  lemul12b  12177  lt2mul2div  12198  lediv12a  12213  tgcl  23292  neissex  23450  alexsublem  24368  alexsubALTlem4  24374  iscmet3  25619  mulsuniflem  28540  ablo4  31157  shscli  31924  mdslmd3i  32939  cvmliftmolem2  36133  mblfinlem4  38671  heibor  38848  ablo4pnp  38907  crngm4  39030  cvratlem  40571  ps-2  40628  cdlemftr3  41715  mzpcompact2lem  43855