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.