Theorem 3adantr1 1168

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant3r1  1181  3ad2antr3  1189  swopo  5514  omeulem1  8413  divmuldiv  11675  imasmnd2  18422  imasgrp2  18690  srgbinomlem2  19777  imasring  19858  abvdiv  20097  mdetunilem9  21769  lly1stc  22647  icccvx  24113  dchrpt  26415  dipsubdir  29210  poimirlem4  35781  fdc  35903  unichnidl  36189  dmncan1  36234  pexmidlem6N  37989  erngdvlem3  39004  erngdvlem3-rN  39012  dvalveclem  39039  dvhvaddass  39111  dvhlveclem  39122  issmflem  44263  prproropf1olem3  44957