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

Metamath Proof Explorer

Theorem rbaibr

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015) (Proof shortened by Wolf Lammen, 19-Jan-2020)

		Ref	Expression
	Hypothesis	baib.1	\|- ( ph <-> ( ps /\ ch ) )
	Assertion	rbaibr	\|- ( ch -> ( ps <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		baib.1	\|- ( ph <-> ( ps /\ ch ) )
2	1	biancomi	\|- ( ph <-> ( ch /\ ps ) )
3	2	baibr	\|- ( ch -> ( ps <-> ph ) )