Theorem 3adantr1 1168

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 1149	. 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 592	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3r1  1181  3ad2antr3  1189  swopo  5599  omeulem1  8585  divmuldiv  11919  imasmnd2  18697  imasgrp2  18975  imasrng  20072  srgbinomlem2  20122  imasring  20219  abvdiv  20589  mdetunilem9  22343  lly1stc  23221  icccvx  24696  dchrpt  27007  dipsubdir  30369  poimirlem4  36796  fdc  36917  unichnidl  37203  dmncan1  37248  pexmidlem6N  39150  erngdvlem3  40165  erngdvlem3-rN  40173  dvalveclem  40200  dvhvaddass  40272  dvhlveclem  40283  issmflem  45742  prproropf1olem3  46472