Theorem orbi2d 792

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 790	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 158	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 790	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 129	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  793  orbi12d  795  dn1dc  963  xorbi2d  1400  eueq2dc  2953  r19.44mv  3563  rexprg  3695  rextpg  3697  exmidsssn  4262  exmidsssnc  4263  swopolem  4370  sowlin  4385  elsucg  4469  elsuc2g  4470  ordsoexmid  4628  poleloe  5101  funopsn  5785  isosolem  5916  freceq2  6502  brdifun  6670  pitric  7469  elinp  7622  prloc  7639  ltexprlemloc  7755  suplocexprlemloc  7869  ltsosr  7912  aptisr  7927  suplocsrlemb  7954  axpre-ltwlin  8031  axpre-suploclemres  8049  axpre-suploc  8050  gt0add  8681  apreap  8695  apreim  8711  elznn0  9422  elznn  9423  peano2z  9443  zindd  9526  elfzp1  10229  fzm1  10257  fzosplitsni  10401  cjap  11332  dvdslelemd  12269  zeo5  12314  lcmval  12500  lcmneg  12511  lcmass  12522  isprm6  12584  infpn2  12942  lringuplu  14073  domneq0  14149  znidom  14534  dedekindeulemloc  15206  dedekindeulemeu  15209  suplociccreex  15211  dedekindicclemloc  15215  dedekindicclemeu  15218  bj-charfunr  15945  bj-nn0sucALT  16113