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 1151	. 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 593	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  1183  3ad2antr3  1191  swopo  5603  omeulem1  8620  divmuldiv  11967  imasmnd2  18787  imasgrp2  19073  imasrng  20174  srgbinomlem2  20224  imasring  20327  abvdiv  20830  mdetunilem9  22626  lly1stc  23504  icccvx  24981  dchrpt  27311  dipsubdir  30867  poimirlem4  37631  fdc  37752  unichnidl  38038  dmncan1  38083  pexmidlem6N  39977  erngdvlem3  40992  erngdvlem3-rN  41000  dvalveclem  41027  dvhvaddass  41099  dvhlveclem  41110  issmflem  46742  prproropf1olem3  47492