7  Two-line rules

7.1 \(\wedge\)I

Proof-formal syntax

Sample instance

\(\wedge\)I: Summary

Info	Description
Subproof	None
Justification	Two lines
Source	Any two (complete) lines
Product	A formula with [\(\wedge\) MLO]
Formal syntax	\(\{\phi, \psi\} \vdash \{(\phi \wedge \psi), (\psi \wedge \phi)\}\)

7.2 \(\to\)E

Proof-formal syntax

Sample instance

\(\to\)E: Summary

Info	Description
Subproofs	None
Justification	Two lines
Source	Two lines: One with [\(\to\) MLO], another with antecedent of the other
Product	Consequent of the first source line
Formal syntax	\(\{ (\phi \to \psi), \phi\} \vdash \psi\)

7.3 \(\leftrightarrow\)E

Proof-formal syntax

Sample instance

\(\leftrightarrow\)E: Summary

Info	Description
Subproofs	None
Justification	Two lines
Source	Two lines: One with [\(\leftrightarrow\) MLO], another with antecedent or consequent of the other
Product	Consequent or antecedent of the first source line
Formal syntax	\(\{ (\phi \leftrightarrow \psi), \phi\} \vdash \psi\), \(\{ (\phi \leftrightarrow \psi), \psi\} \vdash \phi\)

7.4 \(\bot\)I

Proof-formal syntax

Sample instance

\(\bot\)I: Summary

Info	Description
Subproofs	None
Justification	Two lines
Source	Two lines: one the negation of the other
Product	\(\bot\)
Formal syntax	\(\{\phi, \neg \phi\}\vdash \bot\)