claim !P:prop.!Q:prop.!R:prop.P | Q | R -> !P2:prop.(P -> P2) -> (Q -> P2) -> (R -> P2) -> P2