Theorem orbi2d 785

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 143	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	orim2d 783	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 157	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 783	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 128	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 104   \/ wo 703

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1d  786  orbi12d  788  dn1dc  955  xorbi2d  1375  eueq2dc  2903  r19.44mv  3509  rexprg  3635  rextpg  3637  exmidsssn  4188  exmidsssnc  4189  swopolem  4290  sowlin  4305  elsucg  4389  elsuc2g  4390  ordsoexmid  4546  poleloe  5010  isosolem  5803  freceq2  6372  brdifun  6540  pitric  7283  elinp  7436  prloc  7453  ltexprlemloc  7569  suplocexprlemloc  7683  ltsosr  7726  aptisr  7741  suplocsrlemb  7768  axpre-ltwlin  7845  axpre-suploclemres  7863  axpre-suploc  7864  gt0add  8492  apreap  8506  apreim  8522  elznn0  9227  elznn  9228  peano2z  9248  zindd  9330  elfzp1  10028  fzm1  10056  fzosplitsni  10191  cjap  10870  dvdslelemd  11803  zeo5  11847  lcmval  12017  lcmneg  12028  lcmass  12039  isprm6  12101  infpn2  12411  dedekindeulemloc  13391  dedekindeulemeu  13394  suplociccreex  13396  dedekindicclemloc  13400  dedekindicclemeu  13403  bj-charfunr  13845  bj-nn0sucALT  14013