Theorem 3anim3i 1155

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 22	. 2 ⊢ (𝜒 → 𝜒)
2		id 22	. 2 ⊢ (𝜃 → 𝜃)
3		3animi.1	. 2 ⊢ (𝜑 → 𝜓)
4	1, 2, 3	3anim123i 1152	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ 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:  syl3an3  1166  syl3anl3  1417  syl3anr3  1421  elioo4g  13348  ssnn0fi  13936  tmdcn2  24042  axcont  29033  numclwwlk3  30443  minvecolem3  30935  bnj556  35030  bnj557  35031  bnj1145  35123  btwnconn1lem4  36260  btwnconn1lem5  36261  btwnconn1lem6  36262  bj-ceqsalt  37181  bj-ceqsaltv  37182  uhgrimisgrgric  48395  clnbgr3stgrgrlim  48483