ancom-alt

Theorem. Commutativity of conjunction.

Description:

Example illustrating structured proofs and the Deduction Theorem. Compare with ancom.

Arguments:

(pr), (pr),

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Suppose	1.1	()
1.1	siman	1.2
		1.3
1.2, 1.3	>andi	1.4	()
1.4	Therefore	1	(()())
	Suppose	2.1	()
2.1	siman	2.2
		2.3
2.2, 2.3	>andi	2.4	()
2.4	Therefore	2	(()())
1, 2	>bii	3	(()())