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	|- ( ph <-> ps )
Assertion	orbi1i	|- ( ( ph \/ ch ) <-> ( ps \/ ch ) )

Proof

Step	Hyp	Ref	Expression
1		orbi2i.1	|- ( ph <-> ps )
2		orcom	|- ( ( ph \/ ch ) <-> ( ch \/ ph ) )
3	1	orbi2i	|- ( ( ch \/ ph ) <-> ( ch \/ ps ) )
4		orcom	|- ( ( ch \/ ps ) <-> ( ps \/ ch ) )
5	2 3 4	3bitri	|- ( ( ph \/ ch ) <-> ( ps \/ ch ) )