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  5484  omeulem1  8208  divmuldiv  11340  imasmnd2  17948  imasgrp2  18214  srgbinomlem2  19291  imasring  19369  abvdiv  19608  mdetunilem9  21229  lly1stc  22104  icccvx  23554  dchrpt  25843  dipsubdir  28625  poimirlem4  34911  fdc  35035  unichnidl  35324  dmncan1  35369  pexmidlem6N  37126  erngdvlem3  38141  erngdvlem3-rN  38149  dvalveclem  38176  dvhvaddass  38248  dvhlveclem  38259  issmflem  43053  prproropf1olem3  43716