Theorem 3adantr1 1183

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Hypothesis

Ref	Expression
3adantr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3adantr1	⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adantr1

Step	Hyp	Ref	Expression
1		3simpc 1163	. 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 602	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3adant3r1  1196  3ad2antr3  1204  swopo  5566  omeulem1  8551  divmuldiv  11891  imasmnd2  18808  imasgrp2  19097  imasrng  20223  srgbinomlem2  20273  imasring  20375  abvdiv  20875  mdetunilem9  22677  lly1stc  23553  icccvx  25009  dchrpt  27328  dipsubdir  31048  poimirlem4  38120  fdc  38241  unichnidl  38527  dmncan1  38572  pexmidlem6N  40596  erngdvlem3  41611  erngdvlem3-rN  41619  dvalveclem  41646  dvhvaddass  41718  dvhlveclem  41729  issmflem  47298  prproropf1olem3  48108