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	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	orbi1i	⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		orbi2i.1	⊢ ( 𝜑 ↔ 𝜓 )
2		orcom	⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜒 ∨ 𝜑 ) )
3	1	orbi2i	⊢ ( ( 𝜒 ∨ 𝜑 ) ↔ ( 𝜒 ∨ 𝜓 ) )
4		orcom	⊢ ( ( 𝜒 ∨ 𝜓 ) ↔ ( 𝜓 ∨ 𝜒 ) )
5	2 3 4	3bitri	⊢ ( ( 𝜑 ∨ 𝜒 ) ↔ ( 𝜓 ∨ 𝜒 ) )