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  10389  addsrmo  10961  mulsrmo  10962  lemul12b  11975  lt2mul2div  11997  lediv12a  12012  tgcl  22882  neissex  23040  alexsublem  23957  alexsubALTlem4  23963  iscmet3  25218  mulsuniflem  28086  ablo4  30525  shscli  31292  mdslmd3i  32307  brab2d  32583  cvmliftmolem2  35314  mblfinlem4  37699  heibor  37860  ablo4pnp  37919  crngm4  38042  cvratlem  39459  ps-2  39516  cdlemftr3  40603  mzpcompact2lem  42783