Theorem 3anim3i 1172

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 1169	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl3an3  1183  syl3anl3  1441  syl3anr3  1445  elioo4g  13461  ssnn0fi  14051  tmdcn2  24316  axcont  29419  numclwwlk3  30851  minvecolem3  31343  bnj556  35396  bnj557  35397  bnj1145  35489  btwnconn1lem4  36657  btwnconn1lem5  36658  btwnconn1lem6  36659  bj-ceqsalt  37616  bj-ceqsaltv  37617  uhgrimisgrgric  48834  clnbgr3stgrgrlim  48922