Theorem orbi2d 614

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 612	. 2 |- (ph -> ((-. th -> ps) <-> (-. th -> ch)))
3		df-or 224	. 2 |- ((th \/ ps) <-> (-. th -> ps))
4		df-or 224	. 2 |- ((th \/ ch) <-> (-. th -> ch))
5	2, 3, 4	3bitr4g 555	1 |- (ph -> ((th \/ ps) <-> (th \/ ch)))

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

This theorem is referenced by:  orbi1d 615  orbi12d 627  orbidi 743  eueq2 1918  eueq3 1919  sbc2or 1958  ifeq2 2365  elsucg 3036  elsuc2g 3037  ordtri2or 3077  ltsopi 5016  suplem2pr 5162  axlttri 5503  mul0ort 5696  elznn0 6149  elznn 6150  zltp1let 6181  snunioolem 6414  infpn2 7509  sinperlem2 8687

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