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  2908  r19.44mv  3515  rexprg  3641  rextpg  3643  exmidsssn  4197  exmidsssnc  4198  swopolem  4299  sowlin  4314  elsucg  4398  elsuc2g  4399  ordsoexmid  4555  poleloe  5020  isosolem  5815  freceq2  6384  brdifun  6552  pitric  7295  elinp  7448  prloc  7465  ltexprlemloc  7581  suplocexprlemloc  7695  ltsosr  7738  aptisr  7753  suplocsrlemb  7780  axpre-ltwlin  7857  axpre-suploclemres  7875  axpre-suploc  7876  gt0add  8504  apreap  8518  apreim  8534  elznn0  9239  elznn  9240  peano2z  9260  zindd  9342  elfzp1  10040  fzm1  10068  fzosplitsni  10203  cjap  10881  dvdslelemd  11814  zeo5  11858  lcmval  12028  lcmneg  12039  lcmass  12050  isprm6  12112  infpn2  12422  dedekindeulemloc  13648  dedekindeulemeu  13651  suplociccreex  13653  dedekindicclemloc  13657  dedekindicclemeu  13660  bj-charfunr  14102  bj-nn0sucALT  14270