Theorem 3adantr1 1169

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 592	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  1182  3ad2antr3  1190  swopo  5619  omeulem1  8638  divmuldiv  11994  imasmnd2  18809  imasgrp2  19095  imasrng  20204  srgbinomlem2  20254  imasring  20353  abvdiv  20852  mdetunilem9  22647  lly1stc  23525  icccvx  25000  dchrpt  27329  dipsubdir  30880  poimirlem4  37584  fdc  37705  unichnidl  37991  dmncan1  38036  pexmidlem6N  39932  erngdvlem3  40947  erngdvlem3-rN  40955  dvalveclem  40982  dvhvaddass  41054  dvhlveclem  41065  issmflem  46648  prproropf1olem3  47379