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  5574  omeulem1  8570  divmuldiv  11940  imasmnd2  18882  imasgrp2  19179  imasrng  20313  srgbinomlem2  20367  imasring  20472  abvdiv  20996  mdetunilem9  22843  lly1stc  23723  icccvx  25179  dchrpt  27504  dipsubdir  31330  poimirlem4  38374  fdc  38496  unichnidl  38782  dmncan1  38827  pexmidlem6N  40849  erngdvlem3  41864  erngdvlem3-rN  41872  dvalveclem  41899  dvhvaddass  41971  dvhlveclem  41982  issmflem  47556  prproropf1olem3  48406  idomcanl  49263