Theorem orbi2d 736

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 142	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	orim2d 734	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 156	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 734	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 127	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 103   \/ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1d  737  orbi12d  739  dn1dc  901  xorbi2d  1311  eueq2dc  2765  rexprg  3444  rextpg  3446  swopolem  4060  sowlin  4075  elsucg  4159  elsuc2g  4160  ordsoexmid  4305  poleloe  4744  isosolem  5483  freceq2  6003  brdifun  6156  pitric  6511  elinp  6664  prloc  6681  ltexprlemloc  6797  ltsosr  6941  aptisr  6955  axpre-ltwlin  7049  gt0add  7673  apreap  7687  apreim  7703  elznn0  8366  elznn  8367  peano2z  8387  zindd  8465  elfzp1  9089  fzm1  9117  fzosplitsni  9244  cjap  9793  dvdslelemd  10243  zeo5  10288  lcmval  10445  lcmneg  10456  lcmass  10467  isprm6  10526  bj-nn0sucALT  10773