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 ) ) )

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

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  803  orbi12d  805  dn1dc  973  xorbi2d  1429  eueq2dc  2999  r19.44mv  3619  rexprg  3757  rextpg  3759  exmidsssn  4334  exmidsssnc  4335  swopolem  4445  sowlin  4460  elsucg  4544  elsuc2g  4545  ordsoexmid  4704  poleloe  5182  funopsn  5882  isosolem  6020  freceq2  6654  brdifun  6824  papcotr  7603  pitric  7678  elinp  7831  prloc  7848  ltexprlemloc  7964  suplocexprlemloc  8078  ltsosr  8121  aptisr  8136  suplocsrlemb  8163  axpre-ltwlin  8240  axpre-suploclemres  8258  axpre-suploc  8259  gt0add  8891  apreap  8905  apreim  8921  elznn0  9638  elznn  9639  peano2z  9659  zindd  9743  elfzp1  10457  fzm1  10485  fzosplitsni  10632  cjap  11650  dvdslelemd  12588  zeo5  12633  lcmval  12819  lcmneg  12830  lcmass  12841  isprm6  12903  ballotfilemfc0  13210  ballotfilemfcc  13211  infpn2  13325  gzsumsplit0  14125  lringuplu  14476  domneq0  14554  znidom  14964  dedekindeulemloc  15643  dedekindeulemeu  15646  suplociccreex  15648  dedekindicclemloc  15652  dedekindicclemeu  15655  bj-charfunr  16750  bj-nn0sucALT  16918