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  2990  r19.44mv  3604  rexprg  3741  rextpg  3743  exmidsssn  4315  exmidsssnc  4316  swopolem  4426  sowlin  4441  elsucg  4525  elsuc2g  4526  ordsoexmid  4684  poleloe  5162  funopsn  5860  isosolem  5997  freceq2  6624  brdifun  6794  papcotr  7562  pitric  7636  elinp  7789  prloc  7806  ltexprlemloc  7922  suplocexprlemloc  8036  ltsosr  8079  aptisr  8094  suplocsrlemb  8121  axpre-ltwlin  8198  axpre-suploclemres  8216  axpre-suploc  8217  gt0add  8847  apreap  8861  apreim  8877  elznn0  9592  elznn  9593  peano2z  9613  zindd  9696  elfzp1  10406  fzm1  10434  fzosplitsni  10581  cjap  11591  dvdslelemd  12529  zeo5  12574  lcmval  12760  lcmneg  12771  lcmass  12782  isprm6  12844  infpn2  13207  gsumsplit0  14063  lringuplu  14341  domneq0  14418  znidom  14805  dedekindeulemloc  15484  dedekindeulemeu  15487  suplociccreex  15489  dedekindicclemloc  15493  dedekindicclemeu  15496  bj-charfunr  16580  bj-nn0sucALT  16748