Biconditional introduction: Difference between revisions

Revision as of 20:24, 10 March 2012

Revision as of 01:42, 21 September 2012

Line 11:

:<math>(P \to Q), (Q \to P) \vdash (P \leftrightarrow Q)</math>

where <math>\vdash</math> is a [[metalogic]]al symbol meaning that <math>P \leftrightarrow Q</math> is a [[logical consequence|syntactic consequence]] when <math>P \to Q</math> and <math>PQ \to QP</math> are both in a proof;

or as the statement of a truth-functional [[Tautology (logic)|tautology]] or [[theorem]] of propositional logic: