Theorem orbi2i

Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 12-Dec-2012)

	Ref	Expression
Hypothesis	orbi2i.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	orbi2i	$$⊢\left(\chi \vee \phi \right)\leftrightarrow \left(\chi \vee \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		orbi2i.1	$$⊢\phi \leftrightarrow \psi$$
2	1	biimpi	$$⊢\phi \to \psi$$
3	2	orim2i	$$⊢\left(\chi \vee \phi \right)\to \left(\chi \vee \psi \right)$$
4	1	biimpri	$$⊢\psi \to \phi$$
5	4	orim2i	$$⊢\left(\chi \vee \psi \right)\to \left(\chi \vee \phi \right)$$
6	3 5	impbii	$$⊢\left(\chi \vee \phi \right)\leftrightarrow \left(\chi \vee \psi \right)$$