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  10539  addsrmo  11111  mulsrmo  11112  lemul12b  12122  lt2mul2div  12144  lediv12a  12159  tgcl  22992  neissex  23151  alexsublem  24068  alexsubALTlem4  24074  iscmet3  25341  mulsuniflem  28190  ablo4  30579  shscli  31346  mdslmd3i  32361  brab2d  32627  cvmliftmolem2  35267  mblfinlem4  37647  heibor  37808  ablo4pnp  37867  crngm4  37990  cvratlem  39404  ps-2  39461  cdlemftr3  40548  mzpcompact2lem  42739