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  13354  ssnn0fi  13942  tmdcn2  24068  axcont  29063  numclwwlk3  30474  minvecolem3  30966  bnj556  35062  bnj557  35063  bnj1145  35155  btwnconn1lem4  36292  btwnconn1lem5  36293  btwnconn1lem6  36294  bj-ceqsalt  37213  bj-ceqsaltv  37214  uhgrimisgrgric  48425  clnbgr3stgrgrlim  48513