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  5570  omeulem1  8598  divmuldiv  12024  imasmnd2  18977  imasgrp2  19274  imasrng  20408  srgbinomlem2  20462  imasring  20569  abvdiv  21095  mdetunilem9  22944  lly1stc  23824  icccvx  25280  dchrpt  27603  dipsubdir  31459  poimirlem4  38679  fdc  38816  unichnidl  39102  dmncan1  39147  pexmidlem6N  41169  erngdvlem3  42184  erngdvlem3-rN  42192  dvalveclem  42219  dvhvaddass  42291  dvhlveclem  42302  issmflem  47873  prproropf1olem3  48723  idomcanl  49580