Theorem 3adantr1 1216

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  3adant3r1  1239  3ad2antr3  1247  swopo  5274  omeulem1  7930  divmuldiv  11052  imasmnd2  17681  imasgrp2  17885  srgbinomlem2  18896  imasring  18974  abvdiv  19194  mdetunilem9  20795  lly1stc  21671  icccvx  23120  dchrpt  25406  dipsubdir  28259  poimirlem4  33958  fdc  34084  unichnidl  34373  dmncan1  34418  pexmidlem6N  36051  erngdvlem3  37066  erngdvlem3-rN  37074  dvalveclem  37101  dvhvaddass  37173  dvhlveclem  37184  issmflem  41731