Theorem 3anim3i 1170

Description: Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypothesis

Ref	Expression
3animi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
3anim3i	⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

Proof of Theorem 3anim3i

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜒 → 𝜒)
2		id 23	. 2 ⊢ (𝜃 → 𝜃)
3		3animi.1	. 2 ⊢ (𝜑 → 𝜓)
4	1, 2, 3	3anim123i 1167	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  syl3an3  1181  syl3anl3  1439  syl3anr3  1443  elioo4g  13433  ssnn0fi  14021  tmdcn2  24215  axcont  29267  numclwwlk3  30677  minvecolem3  31169  bnj556  35233  bnj557  35234  bnj1145  35326  btwnconn1lem4  36515  btwnconn1lem5  36516  btwnconn1lem6  36517  bj-ceqsalt  37444  bj-ceqsaltv  37445  uhgrimisgrgric  48620  clnbgr3stgrgrlim  48708