I symbolize $T$ as the time-ordered operator and $::$ as normal order symbol. I know that in quantum field theory generally we have:
where $A$ roughly means all possible contractions. I have read a convincing proof.
However when I encounter terms like:
I don't know how to apply Wick theorem. I guess that $A$ now contains only the contractions of pairs not included in the same normal order symbol $::$ (for example the contraction of $\phi_3\phi_4$ is eliminated)
What is the general rules? How can I understand it intuitively?
EDIT: Actually I have found a referrence that states the rules: