Biconditional Introduction/Sequent Form/Proof 1

Theorem

$p \implies q, q \implies p \vdash p \iff q$

Proof

By the tableau method of natural deduction:

$p \implies q, q \implies p \vdash p \iff q$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$p \implies q$	Premise	(None)
2		2	$q \implies p$	Premise	(None)
3		1, 2	$p \iff q$	Biconditional Introduction: $\iff \II$	1, 2

$\blacksquare$