Theorem 3adantr1 1167

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3adant3r1  1180  3ad2antr3  1188  swopo  5505  omeulem1  8375  divmuldiv  11605  imasmnd2  18337  imasgrp2  18605  srgbinomlem2  19692  imasring  19773  abvdiv  20012  mdetunilem9  21677  lly1stc  22555  icccvx  24019  dchrpt  26320  dipsubdir  29111  poimirlem4  35708  fdc  35830  unichnidl  36116  dmncan1  36161  pexmidlem6N  37916  erngdvlem3  38931  erngdvlem3-rN  38939  dvalveclem  38966  dvhvaddass  39038  dvhlveclem  39049  issmflem  44150  prproropf1olem3  44845