Theorem 3adantr1 1165

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant3r1  1178  3ad2antr3  1186  swopo  5478  omeulem1  8202  divmuldiv  11334  imasmnd2  17942  imasgrp2  18208  srgbinomlem2  19285  imasring  19363  abvdiv  19602  mdetunilem9  21223  lly1stc  22098  icccvx  23548  dchrpt  25837  dipsubdir  28619  poimirlem4  34890  fdc  35014  unichnidl  35303  dmncan1  35348  pexmidlem6N  37105  erngdvlem3  38120  erngdvlem3-rN  38128  dvalveclem  38155  dvhvaddass  38227  dvhlveclem  38238  issmflem  42998  prproropf1olem3  43661