Theorem adantrrr 757

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  2ndconst  7153  zorn2lem6  9206  addsrmo  9773  mulsrmo  9774  lemul12b  10759  lt2mul2div  10780  lediv12a  10795  tgcl  20584  neissex  20741  alexsublem  21658  alexsubALTlem4  21664  iscmet3  22899  ablo4  26788  shscli  27560  mdslmd3i  28575  cvmliftmolem2  30518  mblfinlem4  32619  heibor  32790  ablo4pnp  32849  crngm4  32972  cvratlem  33725  ps-2  33782  cdlemftr3  34871  mzpcompact2lem  36332