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  10454  addsrmo  11026  mulsrmo  11027  lemul12b  12039  lt2mul2div  12061  lediv12a  12076  tgcl  22856  neissex  23014  alexsublem  23931  alexsubALTlem4  23937  iscmet3  25193  mulsuniflem  28052  ablo4  30479  shscli  31246  mdslmd3i  32261  brab2d  32535  cvmliftmolem2  35269  mblfinlem4  37654  heibor  37815  ablo4pnp  37874  crngm4  37997  cvratlem  39415  ps-2  39472  cdlemftr3  40559  mzpcompact2lem  42739