Theorem 3adantr1 1166

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  3adant3r1  1179  3ad2antr3  1187  swopo  5448  omeulem1  8191  divmuldiv  11329  imasmnd2  17940  imasgrp2  18206  srgbinomlem2  19284  imasring  19365  abvdiv  19601  mdetunilem9  21225  lly1stc  22101  icccvx  23555  dchrpt  25851  dipsubdir  28631  poimirlem4  35061  fdc  35183  unichnidl  35469  dmncan1  35514  pexmidlem6N  37271  erngdvlem3  38286  erngdvlem3-rN  38294  dvalveclem  38321  dvhvaddass  38393  dvhlveclem  38404  issmflem  43361  prproropf1olem3  44022