Theorem adantrrr 726

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  zorn2lem6  10423  addsrmo  10996  mulsrmo  10997  lemul12b  12010  lt2mul2div  12032  lediv12a  12047  tgcl  22925  neissex  23083  alexsublem  24000  alexsubALTlem4  24006  iscmet3  25261  mulsuniflem  28157  ablo4  30637  shscli  31404  mdslmd3i  32419  brab2d  32694  cvmliftmolem2  35495  mblfinlem4  37905  heibor  38066  ablo4pnp  38125  crngm4  38248  cvratlem  39791  ps-2  39848  cdlemftr3  40935  mzpcompact2lem  43102