Theorem 3adantr1 1188

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3adant3r1  1201  3ad2antr3  1209  swopo  5580  omeulem1  8563  divmuldiv  11910  imasmnd2  18827  imasgrp2  19116  imasrng  20250  srgbinomlem2  20304  imasring  20408  abvdiv  20932  mdetunilem9  22777  lly1stc  23653  icccvx  25109  dchrpt  27431  dipsubdir  31200  poimirlem4  38275  fdc  38396  unichnidl  38682  dmncan1  38727  pexmidlem6N  40749  erngdvlem3  41764  erngdvlem3-rN  41772  dvalveclem  41799  dvhvaddass  41871  dvhlveclem  41882  issmflem  47441  prproropf1olem3  48254  idomcanl  49112