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  1442  syl3anr3  1446  elioo4g  13561  ssnn0fi  14152  tmdcn2  24435  axcont  29581  numclwwlk3  31013  minvecolem3  31505  bnj556  35597  bnj557  35598  bnj1145  35690  acwer1prclem  35850  btwnconn1lem4  37032  btwnconn1lem5  37033  btwnconn1lem6  37034  bj-ceqsalt  37975  bj-ceqsaltv  37976  uhgrimisgrgric  49232  clnbgr3stgrgrlim  49320