Theorem orbi1i

Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993)

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

Proof

Step	Hyp	Ref	Expression
1		orbi2i.1	$$⊢\phi \leftrightarrow \psi$$
2		orcom	$$⊢\left(\phi \vee \chi \right)\leftrightarrow \left(\chi \vee \phi \right)$$
3	1	orbi2i	$$⊢\left(\chi \vee \phi \right)\leftrightarrow \left(\chi \vee \psi \right)$$
4		orcom	$$⊢\left(\chi \vee \psi \right)\leftrightarrow \left(\psi \vee \chi \right)$$
5	2 3 4	3bitri	$$⊢\left(\phi \vee \chi \right)\leftrightarrow \left(\psi \vee \chi \right)$$