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

Metamath Proof Explorer

Theorem biancomd

Description: Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018)

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

Step	Hyp	Ref	Expression
1		biancomd.1	$⊢ φ \to (ψ \leftrightarrow (θ \land χ))$
2		ancom	$⊢ (θ \land χ) \leftrightarrow (χ \land θ)$
3	1 2	bitrdi	$⊢ φ \to (ψ \leftrightarrow (χ \land θ))$