Theorem orbi2d 779

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 143	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	orim2d 777	. 2 |- ( ph -> ( ( th \/ ps ) -> ( th \/ ch ) ) )
4	1	biimprd 157	. . 3 |- ( ph -> ( ch -> ps ) )
5	4	orim2d 777	. 2 |- ( ph -> ( ( th \/ ch ) -> ( th \/ ps ) ) )
6	3, 5	impbid 128	1 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 104   \/ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1d  780  orbi12d  782  dn1dc  944  xorbi2d  1358  eueq2dc  2852  r19.44mv  3452  rexprg  3570  rextpg  3572  exmidsssn  4120  exmidsssnc  4121  swopolem  4222  sowlin  4237  elsucg  4321  elsuc2g  4322  ordsoexmid  4472  poleloe  4933  isosolem  5718  freceq2  6283  brdifun  6449  pitric  7122  elinp  7275  prloc  7292  ltexprlemloc  7408  suplocexprlemloc  7522  ltsosr  7565  aptisr  7580  suplocsrlemb  7607  axpre-ltwlin  7684  axpre-suploclemres  7702  axpre-suploc  7703  gt0add  8328  apreap  8342  apreim  8358  elznn0  9062  elznn  9063  peano2z  9083  zindd  9162  elfzp1  9845  fzm1  9873  fzosplitsni  10005  cjap  10671  dvdslelemd  11530  zeo5  11574  lcmval  11733  lcmneg  11744  lcmass  11755  isprm6  11814  dedekindeulemloc  12755  dedekindeulemeu  12758  suplociccreex  12760  dedekindicclemloc  12764  dedekindicclemeu  12767  bj-nn0sucALT  13165