Theorem 3anim3i 1168

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

Syntax hints:   → wi 4   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  syl3an3  1179  syl3anl3  1435  syl3anr3  1439  elioo4g  13412  ssnn0fi  14000  tmdcn2  24151  axcont  29179  numclwwlk3  30589  minvecolem3  31081  bnj556  35197  bnj557  35198  bnj1145  35290  btwnconn1lem4  36445  btwnconn1lem5  36446  btwnconn1lem6  36447  bj-ceqsalt  37376  bj-ceqsaltv  37377  uhgrimisgrgric  48558  clnbgr3stgrgrlim  48646