Theorem orbi2d 790

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  791  orbi12d  793  dn1dc  960  xorbi2d  1380  eueq2dc  2912  r19.44mv  3519  rexprg  3646  rextpg  3648  exmidsssn  4204  exmidsssnc  4205  swopolem  4307  sowlin  4322  elsucg  4406  elsuc2g  4407  ordsoexmid  4563  poleloe  5030  isosolem  5827  freceq2  6396  brdifun  6564  pitric  7322  elinp  7475  prloc  7492  ltexprlemloc  7608  suplocexprlemloc  7722  ltsosr  7765  aptisr  7780  suplocsrlemb  7807  axpre-ltwlin  7884  axpre-suploclemres  7902  axpre-suploc  7903  gt0add  8532  apreap  8546  apreim  8562  elznn0  9270  elznn  9271  peano2z  9291  zindd  9373  elfzp1  10074  fzm1  10102  fzosplitsni  10237  cjap  10917  dvdslelemd  11851  zeo5  11895  lcmval  12065  lcmneg  12076  lcmass  12087  isprm6  12149  infpn2  12459  lringuplu  13342  dedekindeulemloc  14182  dedekindeulemeu  14185  suplociccreex  14187  dedekindicclemloc  14191  dedekindicclemeu  14194  bj-charfunr  14647  bj-nn0sucALT  14815