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  5585  omeulem1  8576  divmuldiv  11933  imasmnd2  18863  imasgrp2  19152  imasrng  20286  srgbinomlem2  20340  imasring  20445  abvdiv  20969  mdetunilem9  22814  lly1stc  23690  icccvx  25146  dchrpt  27468  dipsubdir  31237  poimirlem4  38315  fdc  38436  unichnidl  38722  dmncan1  38767  pexmidlem6N  40789  erngdvlem3  41804  erngdvlem3-rN  41812  dvalveclem  41839  dvhvaddass  41911  dvhlveclem  41922  issmflem  47481  prproropf1olem3  48294  idomcanl  49152