Theorem 3adantr1 1176

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adant3r1  1189  3ad2antr3  1197  swopo  5537  omeulem1  8507  divmuldiv  11846  imasmnd2  18733  imasgrp2  19022  imasrng  20149  srgbinomlem2  20199  imasring  20301  abvdiv  20801  mdetunilem9  22603  lly1stc  23479  icccvx  24935  dchrpt  27248  dipsubdir  30937  poimirlem4  37991  fdc  38112  unichnidl  38398  dmncan1  38443  pexmidlem6N  40467  erngdvlem3  41482  erngdvlem3-rN  41490  dvalveclem  41517  dvhvaddass  41589  dvhlveclem  41600  issmflem  47170  prproropf1olem3  47980