Theorem orbi2d 798

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  799  orbi12d  801  dn1dc  969  xorbi2d  1425  eueq2dc  2980  r19.44mv  3591  rexprg  3725  rextpg  3727  exmidsssn  4298  exmidsssnc  4299  swopolem  4408  sowlin  4423  elsucg  4507  elsuc2g  4508  ordsoexmid  4666  poleloe  5143  funopsn  5838  isosolem  5975  freceq2  6602  brdifun  6772  pitric  7601  elinp  7754  prloc  7771  ltexprlemloc  7887  suplocexprlemloc  8001  ltsosr  8044  aptisr  8059  suplocsrlemb  8086  axpre-ltwlin  8163  axpre-suploclemres  8181  axpre-suploc  8182  gt0add  8812  apreap  8826  apreim  8842  elznn0  9555  elznn  9556  peano2z  9576  zindd  9659  elfzp1  10369  fzm1  10397  fzosplitsni  10544  cjap  11546  dvdslelemd  12484  zeo5  12529  lcmval  12715  lcmneg  12726  lcmass  12737  isprm6  12799  infpn2  13157  gsumsplit0  14013  lringuplu  14291  domneq0  14368  znidom  14753  dedekindeulemloc  15430  dedekindeulemeu  15433  suplociccreex  15435  dedekindicclemloc  15439  dedekindicclemeu  15442  bj-charfunr  16526  bj-nn0sucALT  16694