Theorem 3adantr1 1212

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3ad2antr3  1220  3adant3r1  1265  swopo  4958  omeulem1  7526  divmuldiv  10576  imasmnd2  17098  imasgrp2  17301  srgbinomlem2  18312  imasring  18390  abvdiv  18608  mdetunilem9  20192  lly1stc  21056  icccvx  22504  dchrpt  24736  dipsubdir  26880  poimirlem4  32366  fdc  32494  unichnidl  32783  dmncan1  32828  pexmidlem6N  34062  erngdvlem3  35079  erngdvlem3-rN  35087  dvalveclem  35115  dvhvaddass  35187  dvhlveclem  35198  issmflem  39396