Rule of Conjunction/Sequent Form/Formulation 2

Theorem

The Rule of Conjunction can be symbolised by the sequent:

$\vdash p \implies \paren {q \implies \paren {p \land q} }$

$\vdash p \implies \paren {q \implies \paren {p \land q} }$
Line	Formula	Rule	Depends upon	Notes
1	$\neg p \lor p$	Law of Excluded Middle
2	$\paren {\neg p \lor p} \implies \paren {p \lor \neg p}$	Axiom $\text A 3$		$\neg p \,/\, p, p \,/\, q$
3	$p \lor \neg p$	Rule $\text {RST} 3$	1, 2
4	$\paren {\neg p \lor \neg q} \lor \neg \paren {\neg p \lor \neg q}$	Rule $\text {RST} 1$	3	$\paren {\neg p \lor \neg q} \,/\, p$
5	$\paren {\neg p \lor \neg q} \lor \paren {p \land q}$	Rule $\text {RST} 2 (1)$
6	$\paren {\paren {\neg p \lor \neg q} \lor \paren {p \land q} } \implies \paren {\neg p \lor \paren {\neg q \lor \paren {p \land q} } }$	Rule of Association		$\neg p \,/\, p, \neg q \,/\, q, \paren {p \land q} \,/\, r$
7	$\neg p \lor \paren {\neg q \lor \paren {p \land q} }$	Rule $\text {RST} 3$	5, 6
8	$p \implies \paren {q \implies \paren {p \land q} }$	Rule $\text {RST} 2 (2)$	7

$\blacksquare$