Theorem 3anim3i 1171

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

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

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 401  df-3an 1104

This theorem is used by:  syl3an3  1182  syl3anl3  1440  syl3anr3  1444  elioo4g  13439  ssnn0fi  14028  tmdcn2  24257  axcont  29337  numclwwlk3  30747  minvecolem3  31239  bnj556  35297  bnj557  35298  bnj1145  35390  btwnconn1lem4  36590  btwnconn1lem5  36591  btwnconn1lem6  36592  bj-ceqsalt  37549  bj-ceqsaltv  37550  uhgrimisgrgric  48724  clnbgr3stgrgrlim  48812