Theorem 3adantr1 1170

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

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

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 1088

This theorem is referenced by:  3adant3r1  1183  3ad2antr3  1191  swopo  5541  omeulem1  8507  divmuldiv  11839  imasmnd2  18697  imasgrp2  18983  imasrng  20110  srgbinomlem2  20160  imasring  20264  abvdiv  20760  mdetunilem9  22562  lly1stc  23438  icccvx  24902  dchrpt  27232  dipsubdir  30872  poimirlem4  37764  fdc  37885  unichnidl  38171  dmncan1  38216  pexmidlem6N  40174  erngdvlem3  41189  erngdvlem3-rN  41197  dvalveclem  41224  dvhvaddass  41296  dvhlveclem  41307  issmflem  46913  prproropf1olem3  47693