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  13537  ssnn0fi  14128  tmdcn2  24408  axcont  29554  numclwwlk3  30986  minvecolem3  31478  bnj556  35530  bnj557  35531  bnj1145  35623  acwer1prclem  35759  btwnconn1lem4  36855  btwnconn1lem5  36856  btwnconn1lem6  36857  bj-ceqsalt  37798  bj-ceqsaltv  37799  uhgrimisgrgric  49029  clnbgr3stgrgrlim  49117