Theorem 3adantr1 1188

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 1168	. 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 605	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3r1  1201  3ad2antr3  1209  swopo  5582  omeulem1  8573  divmuldiv  11932  imasmnd2  18871  imasgrp2  19167  imasrng  20301  srgbinomlem2  20355  imasring  20460  abvdiv  20984  mdetunilem9  22829  lly1stc  23706  icccvx  25162  dchrpt  27484  dipsubdir  31273  poimirlem4  38334  fdc  38456  unichnidl  38742  dmncan1  38787  pexmidlem6N  40809  erngdvlem3  41824  erngdvlem3-rN  41832  dvalveclem  41859  dvhvaddass  41931  dvhlveclem  41942  issmflem  47501  prproropf1olem3  48314  idomcanl  49171