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 593	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3adant3r1  1182  3ad2antr3  1190  swopo  5599  omeulem1  8584  divmuldiv  11916  imasmnd2  18664  imasgrp2  18940  srgbinomlem2  20052  imasring  20147  abvdiv  20449  mdetunilem9  22129  lly1stc  23007  icccvx  24473  dchrpt  26777  dipsubdir  30139  poimirlem4  36578  fdc  36699  unichnidl  36985  dmncan1  37030  pexmidlem6N  38932  erngdvlem3  39947  erngdvlem3-rN  39955  dvalveclem  39982  dvhvaddass  40054  dvhlveclem  40065  issmflem  45522  prproropf1olem3  46252  imasrng  46757