Theorem 3adantr1 1170

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3r1  1183  3ad2antr3  1191  swopo  5572  omeulem1  8594  divmuldiv  11941  imasmnd2  18752  imasgrp2  19038  imasrng  20137  srgbinomlem2  20187  imasring  20290  abvdiv  20789  mdetunilem9  22558  lly1stc  23434  icccvx  24899  dchrpt  27230  dipsubdir  30829  poimirlem4  37648  fdc  37769  unichnidl  38055  dmncan1  38100  pexmidlem6N  39994  erngdvlem3  41009  erngdvlem3-rN  41017  dvalveclem  41044  dvhvaddass  41116  dvhlveclem  41127  issmflem  46756  prproropf1olem3  47519