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  20277  imasring  20379  abvdiv  20878  mdetunilem9  22680  lly1stc  23556  icccvx  25012  dchrpt  27331  dipsubdir  31051  poimirlem4  38123  fdc  38244  unichnidl  38530  dmncan1  38575  pexmidlem6N  40599  erngdvlem3  41614  erngdvlem3-rN  41622  dvalveclem  41649  dvhvaddass  41721  dvhlveclem  41732  issmflem  47301  prproropf1olem3  48111