Theorem adantrrr 735

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  zorn2lem6  10455  addsrmo  11028  mulsrmo  11029  lemul12b  12045  lt2mul2div  12067  lediv12a  12082  tgcl  23009  neissex  23167  alexsublem  24084  alexsubALTlem4  24090  iscmet3  25335  mulsuniflem  28219  ablo4  30699  shscli  31466  mdslmd3i  32481  brab2d  32757  cvmliftmolem2  35596  mblfinlem4  38123  heibor  38284  ablo4pnp  38343  crngm4  38466  cvratlem  40009  ps-2  40066  cdlemftr3  41153  mzpcompact2lem  43296