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 1090  19.41 1095  unass 2187  ordtri2or 3077  onzsl 3117  tz7.48lem 3955  zorn 4797  entri2 4840  leloet 5518  xrleloet 5557  arch 6071  elznn0nn 6148  snunioolem 6414  elfzp1 6510  efgt0 7404  fctop2 7651  efif1lem5 8734  grothprim 8783  chrelat2 10292

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