Theorem 3anim3i 1155

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 22	. 2 ⊢ (𝜒 → 𝜒)
2		id 22	. 2 ⊢ (𝜃 → 𝜃)
3		3animi.1	. 2 ⊢ (𝜑 → 𝜓)
4	1, 2, 3	3anim123i 1152	1 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl3an3  1166  syl3anl3  1417  syl3anr3  1421  elioo4g  13326  ssnn0fi  13912  tmdcn2  24037  axcont  29053  numclwwlk3  30464  minvecolem3  30955  bnj556  35058  bnj557  35059  bnj1145  35151  btwnconn1lem4  36286  btwnconn1lem5  36287  btwnconn1lem6  36288  bj-ceqsalt  37089  bj-ceqsaltv  37090  uhgrimisgrgric  48244  clnbgr3stgrgrlim  48332