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  2934  r19.44mv  3542  rexprg  3671  rextpg  3673  exmidsssn  4232  exmidsssnc  4233  swopolem  4337  sowlin  4352  elsucg  4436  elsuc2g  4437  ordsoexmid  4595  poleloe  5066  isosolem  5868  freceq2  6448  brdifun  6616  pitric  7383  elinp  7536  prloc  7553  ltexprlemloc  7669  suplocexprlemloc  7783  ltsosr  7826  aptisr  7841  suplocsrlemb  7868  axpre-ltwlin  7945  axpre-suploclemres  7963  axpre-suploc  7964  gt0add  8594  apreap  8608  apreim  8624  elznn0  9335  elznn  9336  peano2z  9356  zindd  9438  elfzp1  10141  fzm1  10169  fzosplitsni  10305  cjap  11053  dvdslelemd  11988  zeo5  12032  lcmval  12204  lcmneg  12215  lcmass  12226  isprm6  12288  infpn2  12616  lringuplu  13695  domneq0  13771  znidom  14156  dedekindeulemloc  14798  dedekindeulemeu  14801  suplociccreex  14803  dedekindicclemloc  14807  dedekindicclemeu  14810  bj-charfunr  15372  bj-nn0sucALT  15540