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  8581  divmuldiv  11913  imasmnd2  18661  imasgrp2  18937  srgbinomlem2  20049  imasring  20142  abvdiv  20444  mdetunilem9  22121  lly1stc  22999  icccvx  24465  dchrpt  26767  dipsubdir  30096  poimirlem4  36487  fdc  36608  unichnidl  36894  dmncan1  36939  pexmidlem6N  38841  erngdvlem3  39856  erngdvlem3-rN  39864  dvalveclem  39891  dvhvaddass  39963  dvhlveclem  39974  issmflem  45433  prproropf1olem3  46163  imasrng  46668