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 482	. 2 ⊢ ((𝜒 ∧ 𝜏) → 𝜒)
2		adantr2.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylanr2 683	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  10414  addsrmo  10986  mulsrmo  10987  lemul12b  11999  lt2mul2div  12021  lediv12a  12036  tgcl  22872  neissex  23030  alexsublem  23947  alexsubALTlem4  23953  iscmet3  25209  mulsuniflem  28075  ablo4  30512  shscli  31279  mdslmd3i  32294  brab2d  32568  cvmliftmolem2  35254  mblfinlem4  37639  heibor  37800  ablo4pnp  37859  crngm4  37982  cvratlem  39400  ps-2  39457  cdlemftr3  40544  mzpcompact2lem  42724