Theorem orbi1i 215

Description: Inference adding a right disjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.oa	|- (ph <-> ps)

Assertion

Ref	Expression
orbi1i	|- ((ph \/ ch) <-> (ps \/ ch))

Proof of Theorem orbi1i

Step	Hyp	Ref	Expression
1		orcom 209	. 2 |- ((ph \/ ch) <-> (ch \/ ph))
2		bi.oa	. . 3 |- (ph <-> ps)
3	2	orbi2i 214	. 2 |- ((ch \/ ph) <-> (ch \/ ps))
4		orcom 209	. 2 |- ((ch \/ ps) <-> (ps \/ ch))
5	1, 3, 4	3bitr 155	1 |- ((ph \/ ch) <-> (ps \/ ch))

Syntax hints:   <-> wb 127   \/ wo 195

This theorem is referenced by:  orbi12i 216  orordi 222  19.45 769  19.41 774  unass 1615  ordtri2or 2328  onzsl 2367  tz7.48lem 2993  zorn2 3612  entri2 3646  leloet 4284  arch 4521  elznn0nn 4575  chrelat2 5758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org