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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  syl3an3  1166  syl3anl3  1415  syl3anr3  1419  elioo4g  13384  ssnn0fi  13950  tmdcn2  23593  axcont  28265  numclwwlk3  29669  minvecolem3  30160  bnj556  33942  bnj557  33943  bnj1145  34035  btwnconn1lem4  35093  btwnconn1lem5  35094  btwnconn1lem6  35095  bj-ceqsalt  35814  bj-ceqsaltv  35815