Theorem orbi1d 614

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 613	. 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 554	1 |- (ph -> ((ps \/ th) <-> (ch \/ th)))

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

This theorem is referenced by:  orbi1 619  orbi12d 626  dedlema 761  eueq2 1914  eueq3 1915  uneq1 2173  r19.45zv 2348  ifeq1 2360  lelttrit 5604  mul0ort 5673  seq1bnd 6855  bccl2t 6917  reeff1o 7376  pilem1 8609  axgroth2 8717  axgroth3 8718  h1datomt 9445

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