9  Two-subproof rules

9.1 \(\leftrightarrow\)I

Proof-formal syntax

Sample instance

\(\leftrightarrow\)I: Summary

Info	Description
Subproofs	\([ \phi \vdash \psi], [\psi \vdash \phi]\)
Justification	Two subproofs (as ranges)
Source	The subproofs
Product	A formula with [\(\leftrightarrow\) MLO] whose antecedent and consequent are the first and last lines of the first subproof respectively (=last and first lines, inversely, of the second subproof)
Formal syntax	\(\{[\phi \vdash \psi], [\psi \vdash \phi]\} \vdash (\phi \leftrightarrow \psi)\)

9.2 \(\vee\)E

Proof-formal syntax

Sample instance

9.2.1 \(\vee\)E: Summary

Info	Description
Subproofs	\([\phi \vdash \chi], [\psi \vdash \chi]\), given \((\phi \vee \psi)\)
Justification	Two subroofs (as ranges) and one line
Source	The subproofs and the line with [\(\vee\) MLO]
Product	The formula that is the last line of the two subproofs
Formal syntax	\(\{ (\phi \vee \psi), [\phi \vdash \chi], [\psi \vdash \chi]\} \vdash \chi\)