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  2937  r19.44mv  3546  rexprg  3675  rextpg  3677  exmidsssn  4236  exmidsssnc  4237  swopolem  4341  sowlin  4356  elsucg  4440  elsuc2g  4441  ordsoexmid  4599  poleloe  5070  isosolem  5874  freceq2  6460  brdifun  6628  pitric  7405  elinp  7558  prloc  7575  ltexprlemloc  7691  suplocexprlemloc  7805  ltsosr  7848  aptisr  7863  suplocsrlemb  7890  axpre-ltwlin  7967  axpre-suploclemres  7985  axpre-suploc  7986  gt0add  8617  apreap  8631  apreim  8647  elznn0  9358  elznn  9359  peano2z  9379  zindd  9461  elfzp1  10164  fzm1  10192  fzosplitsni  10328  cjap  11088  dvdslelemd  12025  zeo5  12070  lcmval  12256  lcmneg  12267  lcmass  12278  isprm6  12340  infpn2  12698  lringuplu  13828  domneq0  13904  znidom  14289  dedekindeulemloc  14939  dedekindeulemeu  14942  suplociccreex  14944  dedekindicclemloc  14948  dedekindicclemeu  14951  bj-charfunr  15540  bj-nn0sucALT  15708