Theorem adantrrr 725

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 683	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 210  df-an 400

This theorem is referenced by:  zorn2lem6  10080  addsrmo  10652  mulsrmo  10653  lemul12b  11654  lt2mul2div  11675  lediv12a  11690  tgcl  21820  neissex  21978  alexsublem  22895  alexsubALTlem4  22901  iscmet3  24144  ablo4  28585  shscli  29352  mdslmd3i  30367  cvmliftmolem2  32911  mblfinlem4  35503  heibor  35665  ablo4pnp  35724  crngm4  35847  cvratlem  37121  ps-2  37178  cdlemftr3  38265  mzpcompact2lem  40217