Enter a formula of propositional or predicate logic (without identity). Use LaTeX commands or the buttons on top of the text field to insert logical symbols.

Examples (click to see the proof):

More detailed instructions and explanations are available here.