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  6668  brdifun  6838  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  9670  elznn  9671  peano2z  9691  zindd  9775  elfzp1  10496  fzm1  10524  fzosplitsni  10671  cjap  11694  dvdslelemd  12635  zeo5  12680  lcmval  12866  lcmneg  12877  lcmass  12888  isprm6  12951  ballotfilemfc0  13290  ballotfilemfcc  13291  infpn2  13405  gzsumsplit0  14238  lringuplu  14612  domneq0  14690  znidom  15101  dedekindeulemloc  15845  dedekindeulemeu  15848  suplociccreex  15850  dedekindicclemloc  15854  dedekindicclemeu  15857  bj-charfunr  17041  bj-nn0sucALT  17209