Theorem orbi2d 791

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

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

Assertion

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

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		orbid.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 144	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	orim2d 789	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 158	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 789	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 129	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  792  orbi12d  794  dn1dc  962  xorbi2d  1391  eueq2dc  2933  r19.44mv  3541  rexprg  3670  rextpg  3672  exmidsssn  4231  exmidsssnc  4232  swopolem  4336  sowlin  4351  elsucg  4435  elsuc2g  4436  ordsoexmid  4594  poleloe  5065  isosolem  5867  freceq2  6446  brdifun  6614  pitric  7381  elinp  7534  prloc  7551  ltexprlemloc  7667  suplocexprlemloc  7781  ltsosr  7824  aptisr  7839  suplocsrlemb  7866  axpre-ltwlin  7943  axpre-suploclemres  7961  axpre-suploc  7962  gt0add  8592  apreap  8606  apreim  8622  elznn0  9332  elznn  9333  peano2z  9353  zindd  9435  elfzp1  10138  fzm1  10166  fzosplitsni  10302  cjap  11050  dvdslelemd  11985  zeo5  12029  lcmval  12201  lcmneg  12212  lcmass  12223  isprm6  12285  infpn2  12613  lringuplu  13692  domneq0  13768  znidom  14145  dedekindeulemloc  14773  dedekindeulemeu  14776  suplociccreex  14778  dedekindicclemloc  14782  dedekindicclemeu  14785  bj-charfunr  15302  bj-nn0sucALT  15470