Theorem 3anim3i 1250

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl3anl3  1376  syl3anr3  1380  elioo4g  12234  ssnn0fi  12784  tmdcn2  21893  axcont  25856  1ewlk  26976  1pthon2ve  27014  numclwwlk3OLD  27242  numclwwlk3  27243  minvecolem3  27732  bnj556  30970  bnj557  30971  bnj1145  31061  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  bj-ceqsalt  32875  bj-ceqsaltv  32876