Theorem 3adantr1 1171

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 1151	. 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2		3adantr.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylan2 594	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  1184  3ad2antr3  1192  swopo  5544  omeulem1  8511  divmuldiv  11849  imasmnd2  18736  imasgrp2  19025  imasrng  20152  srgbinomlem2  20202  imasring  20304  abvdiv  20800  mdetunilem9  22598  lly1stc  23474  icccvx  24930  dchrpt  27247  dipsubdir  30937  poimirlem4  37962  fdc  38083  unichnidl  38369  dmncan1  38414  pexmidlem6N  40438  erngdvlem3  41453  erngdvlem3-rN  41461  dvalveclem  41488  dvhvaddass  41560  dvhlveclem  41571  issmflem  47176  prproropf1olem3  47980