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  5527  zorn2lem6  10503  addsrmo  11076  mulsrmo  11077  lemul12b  12090  lt2mul2div  12111  lediv12a  12126  tgcl  23163  neissex  23321  alexsublem  24238  alexsubALTlem4  24244  iscmet3  25489  mulsuniflem  28379  ablo4  30939  shscli  31706  mdslmd3i  32721  cvmliftmolem2  35795  mblfinlem4  38352  heibor  38513  ablo4pnp  38572  crngm4  38695  cvratlem  40236  ps-2  40293  cdlemftr3  41380  mzpcompact2lem  43523