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  13506  ssnn0fi  14096  tmdcn2  24369  axcont  29487  numclwwlk3  30919  minvecolem3  31411  bnj556  35464  bnj557  35465  bnj1145  35557  btwnconn1lem4  36777  btwnconn1lem5  36778  btwnconn1lem6  36779  bj-ceqsalt  37720  bj-ceqsaltv  37721  uhgrimisgrgric  48951  clnbgr3stgrgrlim  49039