Theorem orbi2d 797

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  798  orbi12d  800  dn1dc  968  xorbi2d  1424  eueq2dc  2979  r19.44mv  3589  rexprg  3721  rextpg  3723  exmidsssn  4292  exmidsssnc  4293  swopolem  4402  sowlin  4417  elsucg  4501  elsuc2g  4502  ordsoexmid  4660  poleloe  5136  funopsn  5830  isosolem  5965  freceq2  6559  brdifun  6729  pitric  7541  elinp  7694  prloc  7711  ltexprlemloc  7827  suplocexprlemloc  7941  ltsosr  7984  aptisr  7999  suplocsrlemb  8026  axpre-ltwlin  8103  axpre-suploclemres  8121  axpre-suploc  8122  gt0add  8753  apreap  8767  apreim  8783  elznn0  9494  elznn  9495  peano2z  9515  zindd  9598  elfzp1  10307  fzm1  10335  fzosplitsni  10482  cjap  11484  dvdslelemd  12422  zeo5  12467  lcmval  12653  lcmneg  12664  lcmass  12675  isprm6  12737  infpn2  13095  gsumsplit0  13951  lringuplu  14229  domneq0  14305  znidom  14690  dedekindeulemloc  15362  dedekindeulemeu  15365  suplociccreex  15367  dedekindicclemloc  15371  dedekindicclemeu  15374  bj-charfunr  16456  bj-nn0sucALT  16624