Theorem 3adantr1 1171

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

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

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 1089

This theorem is referenced by:  3adant3r1  1184  3ad2antr3  1192  swopo  5551  omeulem1  8519  divmuldiv  11853  imasmnd2  18711  imasgrp2  18997  imasrng  20124  srgbinomlem2  20174  imasring  20278  abvdiv  20774  mdetunilem9  22576  lly1stc  23452  icccvx  24916  dchrpt  27246  dipsubdir  30936  poimirlem4  37875  fdc  37996  unichnidl  38282  dmncan1  38327  pexmidlem6N  40351  erngdvlem3  41366  erngdvlem3-rN  41374  dvalveclem  41401  dvhvaddass  41473  dvhlveclem  41484  issmflem  47085  prproropf1olem3  47865