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  2925  r19.44mv  3532  rexprg  3659  rextpg  3661  exmidsssn  4220  exmidsssnc  4221  swopolem  4323  sowlin  4338  elsucg  4422  elsuc2g  4423  ordsoexmid  4579  poleloe  5046  isosolem  5846  freceq2  6419  brdifun  6587  pitric  7351  elinp  7504  prloc  7521  ltexprlemloc  7637  suplocexprlemloc  7751  ltsosr  7794  aptisr  7809  suplocsrlemb  7836  axpre-ltwlin  7913  axpre-suploclemres  7931  axpre-suploc  7932  gt0add  8561  apreap  8575  apreim  8591  elznn0  9299  elznn  9300  peano2z  9320  zindd  9402  elfzp1  10104  fzm1  10132  fzosplitsni  10267  cjap  10950  dvdslelemd  11884  zeo5  11928  lcmval  12098  lcmneg  12109  lcmass  12120  isprm6  12182  infpn2  12510  lringuplu  13560  dedekindeulemloc  14574  dedekindeulemeu  14577  suplociccreex  14579  dedekindicclemloc  14583  dedekindicclemeu  14586  bj-charfunr  15040  bj-nn0sucALT  15208