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  13538  ssnn0fi  14129  tmdcn2  24409  axcont  29555  numclwwlk3  30987  minvecolem3  31479  bnj556  35531  bnj557  35532  bnj1145  35624  acwer1prclem  35760  btwnconn1lem4  36856  btwnconn1lem5  36857  btwnconn1lem6  36858  bj-ceqsalt  37799  bj-ceqsaltv  37800  uhgrimisgrgric  49030  clnbgr3stgrgrlim  49118