Theorem adantrrr 737

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  brab2d  5524  zorn2lem6  10486  addsrmo  11059  mulsrmo  11060  lemul12b  12073  lt2mul2div  12094  lediv12a  12109  tgcl  23107  neissex  23265  alexsublem  24182  alexsubALTlem4  24188  iscmet3  25433  mulsuniflem  28320  ablo4  30880  shscli  31647  mdslmd3i  32662  cvmliftmolem2  35752  mblfinlem4  38289  heibor  38450  ablo4pnp  38509  crngm4  38632  cvratlem  40173  ps-2  40230  cdlemftr3  41317  mzpcompact2lem  43462