com12i

Theorem. Inference that swaps (commutes) antecedents in an implication.

Arguments:

(pr), (pr), (pr),

Hypotheses:

(())

Assertions:

(())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	(())
	ax1	2	(())
1	ax2	3	(()())
2, 3	syl	4	(())