Theorem orbi2d 612

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

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

This theorem is referenced by:  orbi1d 613  orbi12d 625  orbidi 741  eueq2 1909  eueq3 1910  sbc2or 1948  ifeq2 2355  elsucg 3026  elsuc2g 3027  ordtri2or 3067  ltsopi 4988  suplem2pr 5134  axlttri 5475  mul0ort 5665  elznn0 6096  elznn 6097  zltp1let 6128  snunioolem 6347  infpn2 7452  sinperlem2 8606

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