Theorem orbi1d 613

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

Hypothesis

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

Assertion

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

Proof of Theorem orbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	orbi2d 612	. 2 |- (ph -> ((th \/ ps) <-> (th \/ ch)))
3		orcom 246	. 2 |- ((ps \/ th) <-> (th \/ ps))
4		orcom 246	. 2 |- ((ch \/ th) <-> (th \/ ch))
5	2, 3, 4	3bitr4g 553	1 |- (ph -> ((ps \/ th) <-> (ch \/ th)))

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

This theorem is referenced by:  orbi1 618  orbi12d 625  dedlema 760  eueq2 1909  eueq3 1910  uneq1 2167  r19.45zv 2342  ifeq1 2354  lelttrit 5596  mul0ort 5665  seq1bnd 6847  bccl2t 6909  reeff1o 7368  pilem1 8590  axgroth2 8717  axgroth3 8718  h1datomt 9422

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  df-an 225

Copyright terms: Public domain