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

Metamath Proof Explorer

Theorem biorfd

Description: A wff is equivalent to its disjunction with falsehood, deduction form. (Contributed by Peter Mazsa, 22-Aug-2023)

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

Step	Hyp	Ref	Expression
1		biorfd.1	$⊢ φ \to \neg ψ$
2		biorf	$⊢ \neg ψ \to (χ \leftrightarrow (ψ \lor χ))$
3	1 2	syl	$⊢ φ \to (χ \leftrightarrow (ψ \lor χ))$