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  5819  isosolem  5954  freceq2  6545  brdifun  6715  pitric  7519  elinp  7672  prloc  7689  ltexprlemloc  7805  suplocexprlemloc  7919  ltsosr  7962  aptisr  7977  suplocsrlemb  8004  axpre-ltwlin  8081  axpre-suploclemres  8099  axpre-suploc  8100  gt0add  8731  apreap  8745  apreim  8761  elznn0  9472  elznn  9473  peano2z  9493  zindd  9576  elfzp1  10280  fzm1  10308  fzosplitsni  10453  cjap  11433  dvdslelemd  12370  zeo5  12415  lcmval  12601  lcmneg  12612  lcmass  12623  isprm6  12685  infpn2  13043  lringuplu  14176  domneq0  14252  znidom  14637  dedekindeulemloc  15309  dedekindeulemeu  15312  suplociccreex  15314  dedekindicclemloc  15318  dedekindicclemeu  15321  bj-charfunr  16256  bj-nn0sucALT  16424