Theorem 3adantr1 1186

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3adant3r1  1199  3ad2antr3  1207  swopo  5581  omeulem1  8566  divmuldiv  11914  imasmnd2  18831  imasgrp2  19120  imasrng  20254  srgbinomlem2  20308  imasring  20411  abvdiv  20909  mdetunilem9  22745  lly1stc  23621  icccvx  25077  dchrpt  27396  dipsubdir  31140  poimirlem4  38162  fdc  38283  unichnidl  38569  dmncan1  38614  pexmidlem6N  40638  erngdvlem3  41653  erngdvlem3-rN  41661  dvalveclem  41688  dvhvaddass  41760  dvhlveclem  41771  issmflem  47332  prproropf1olem3  48142