Theorem orbi2d 802

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi1d  803  orbi12d  805  dn1dc  973  xorbi2d  1429  eueq2dc  2999  r19.44mv  3622  rexprg  3761  rextpg  3763  exmidsssn  4341  exmidsssnc  4342  swopolem  4452  sowlin  4467  elsucg  4551  elsuc2g  4552  ordsoexmid  4711  poleloe  5190  funopsn  5894  isosolem  6033  freceq2  6669  brdifun  6839  papcotr  7619  pitric  7694  elinp  7847  prloc  7864  ltexprlemloc  7980  suplocexprlemloc  8094  ltsosr  8137  aptisr  8152  suplocsrlemb  8179  axpre-ltwlin  8256  axpre-suploclemres  8274  axpre-suploc  8275  gt0add  8909  apreap  8923  apreim  8939  elznn0  9668  elznn  9669  peano2z  9689  zindd  9774  elfzp1  10495  fzm1  10523  fzosplitsni  10670  cjap  11693  dvdslelemd  12634  zeo5  12679  lcmval  12865  lcmneg  12876  lcmass  12887  isprm6  12950  ballotfilemfc0  13289  ballotfilemfcc  13290  infpn2  13404  gzsumsplit0  14237  lringuplu  14611  domneq0  14689  znidom  15100  dedekindeulemloc  15862  dedekindeulemeu  15865  suplociccreex  15867  dedekindicclemloc  15871  dedekindicclemeu  15874  bj-charfunr  17058  bj-nn0sucALT  17226