Theorem orbi2d 798

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  799  orbi12d  801  dn1dc  969  xorbi2d  1425  eueq2dc  2993  r19.44mv  3608  rexprg  3746  rextpg  3748  exmidsssn  4320  exmidsssnc  4321  swopolem  4431  sowlin  4446  elsucg  4530  elsuc2g  4531  ordsoexmid  4689  poleloe  5167  funopsn  5865  isosolem  6003  freceq2  6637  brdifun  6807  papcotr  7577  pitric  7652  elinp  7805  prloc  7822  ltexprlemloc  7938  suplocexprlemloc  8052  ltsosr  8095  aptisr  8110  suplocsrlemb  8137  axpre-ltwlin  8214  axpre-suploclemres  8232  axpre-suploc  8233  gt0add  8864  apreap  8878  apreim  8894  elznn0  9609  elznn  9610  peano2z  9630  zindd  9714  elfzp1  10428  fzm1  10456  fzosplitsni  10603  cjap  11616  dvdslelemd  12554  zeo5  12599  lcmval  12785  lcmneg  12796  lcmass  12807  isprm6  12869  ballotfilemfc0  13176  ballotfilemfcc  13177  infpn2  13291  gsumsplit0  14099  lringuplu  14441  domneq0  14519  znidom  14931  dedekindeulemloc  15610  dedekindeulemeu  15613  suplociccreex  15615  dedekindicclemloc  15619  dedekindicclemeu  15622  bj-charfunr  16706  bj-nn0sucALT  16874