Theorem orbi2d 704

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 132	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	orim2d 702	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 147	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 702	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 120	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 98   \/ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orbi1d  705  orbi12d  707  dn1dc  867  xorbi2d  1271  eueq2dc  2714  rexprg  3422  rextpg  3424  swopolem  4042  sowlin  4057  elsucg  4141  elsuc2g  4142  ordsoexmid  4286  poleloe  4724  isosolem  5463  freceq2  5980  brdifun  6133  pitric  6419  elinp  6572  prloc  6589  ltexprlemloc  6705  ltsosr  6849  aptisr  6863  axpre-ltwlin  6957  gt0add  7564  apreap  7578  apreim  7594  elznn0  8260  elznn  8261  peano2z  8281  zindd  8356  elfzp1  8934  fzm1  8962  fzosplitsni  9091  cjap  9506  bj-nn0sucALT  10103