\[u2200] A ^ \[u2203] P ^ \[u2200] B ^ [ B \[u2208] P \[u21D4] \[u2200] C ^ ( C \[u2208] B \[u21D2] C \[u2208] A ) ]