Theorem orbi1i 256

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

Hypothesis

Ref	Expression
orbi2i.1	|- (ph <-> ps)

Assertion

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

Proof of Theorem orbi1i

Step	Hyp	Ref	Expression
1		orcom 246	. 2 |- ((ph \/ ch) <-> (ch \/ ph))
2		orbi2i.1	. . 3 |- (ph <-> ps)
3	2	orbi2i 255	. 2 |- ((ch \/ ph) <-> (ch \/ ps))
4		orcom 246	. 2 |- ((ch \/ ps) <-> (ps \/ ch))
5	1, 3, 4	3bitr 177	1 |- ((ph \/ ch) <-> (ps \/ ch))

Syntax hints:   <-> wb 146   \/ wo 222

This theorem is referenced by:  orbi12i 257  orordi 266  pm4.54 309  19.45 1089  19.41 1094  unass 2184  ordtri2or 3073  onzsl 3113  tz7.48lem 3950  zorn 4780  entri2 4823  leloet 5501  xrleloet 5540  arch 6028  elznn0nn 6105  snunioolem 6360  elfzp1 6455  efgt0 7362  fctop2 7611  efif1lem5 8684  grothprim 8738  chrelat2 10248

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

This theorem depends on definitions:  df-bi 147  df-or 224

Copyright terms: Public domain