Theorem adantrrr 721

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 679	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 206  df-an 396

This theorem is referenced by:  zorn2lem6  10188  addsrmo  10760  mulsrmo  10761  lemul12b  11762  lt2mul2div  11783  lediv12a  11798  tgcl  22027  neissex  22186  alexsublem  23103  alexsubALTlem4  23109  iscmet3  24362  ablo4  28813  shscli  29580  mdslmd3i  30595  cvmliftmolem2  33144  mblfinlem4  35744  heibor  35906  ablo4pnp  35965  crngm4  36088  cvratlem  37362  ps-2  37419  cdlemftr3  38506  mzpcompact2lem  40489