Theorem orbi2d 795

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  796  orbi12d  798  dn1dc  966  xorbi2d  1422  eueq2dc  2976  r19.44mv  3586  rexprg  3718  rextpg  3720  exmidsssn  4286  exmidsssnc  4287  swopolem  4396  sowlin  4411  elsucg  4495  elsuc2g  4496  ordsoexmid  4654  poleloe  5128  funopsn  5817  isosolem  5948  freceq2  6539  brdifun  6707  pitric  7508  elinp  7661  prloc  7678  ltexprlemloc  7794  suplocexprlemloc  7908  ltsosr  7951  aptisr  7966  suplocsrlemb  7993  axpre-ltwlin  8070  axpre-suploclemres  8088  axpre-suploc  8089  gt0add  8720  apreap  8734  apreim  8750  elznn0  9461  elznn  9462  peano2z  9482  zindd  9565  elfzp1  10268  fzm1  10296  fzosplitsni  10441  cjap  11417  dvdslelemd  12354  zeo5  12399  lcmval  12585  lcmneg  12596  lcmass  12607  isprm6  12669  infpn2  13027  lringuplu  14160  domneq0  14236  znidom  14621  dedekindeulemloc  15293  dedekindeulemeu  15296  suplociccreex  15298  dedekindicclemloc  15302  dedekindicclemeu  15305  bj-charfunr  16173  bj-nn0sucALT  16341