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 1086  19.41 1091  unass 2177  ordtri2or 3067  onzsl 3107  tz7.48lem 3940  zorn 4769  entri2 4812  leloet 5491  xrleloet 5530  arch 6018  elznn0nn 6095  snunioolem 6347  elfzp1 6442  efgt0 7345  fctop2 7593  efif1lem5 8649  grothprim 8722  chrelat2 10200

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