This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bicomd

Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993)

		Ref	Expression
	Hypothesis	bicomd.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	bicomd	$⊢ φ \to (χ \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		bicomd.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		bicom	$⊢ (ψ \leftrightarrow χ) \leftrightarrow (χ \leftrightarrow ψ)$
3	1 2	sylib	$⊢ φ \to (χ \leftrightarrow ψ)$