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

Metamath Proof Explorer

Theorem orbi2d

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993)

		Ref	Expression
	Hypothesis	bid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	orbi2d	$⊢ φ \to ((θ \lor ψ) \leftrightarrow (θ \lor χ))$

Step	Hyp	Ref	Expression
1		bid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	imbi2d	$⊢ φ \to ((\neg θ \to ψ) \leftrightarrow (\neg θ \to χ))$
3		df-or	$⊢ (θ \lor ψ) \leftrightarrow (\neg θ \to ψ)$
4		df-or	$⊢ (θ \lor χ) \leftrightarrow (\neg θ \to χ)$
5	2 3 4	3bitr4g	$⊢ φ \to ((θ \lor ψ) \leftrightarrow (θ \lor χ))$