Theorem orbi2d 625

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

Hypothesis

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

Assertion

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

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	imbi2d 623	. 2 |- (ph -> ((-. th -> ps) <-> (-. th -> ch)))
3		df-or 231	. 2 |- ((th \/ ps) <-> (-. th -> ps))
4		df-or 231	. 2 |- ((th \/ ch) <-> (-. th -> ch))
5	2, 3, 4	3bitr4g 566	1 |- (ph -> ((th \/ ps) <-> (th \/ ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 153   \/ wo 229

This theorem is referenced by:  orbi1d 626  orbi12d 638  orbidi 755  eueq2 1965  eueq3 1966  sbc2or 2008  ifeq2 2417  elsucg 3093  elsuc2g 3094  ordtri2or 3134  ltsopi 5081  suplem2pr 5227  axlttri 5568  mul0or 5761  rpneg 6125  elznn0 6231  elznn 6232  zltp1le 6263  snunioolem 6440  infpn2 7601  sinperlem2 8770

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 154  df-or 231  df-an 232

Copyright terms: Public domain