Theorem orbi2d 792

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  793  orbi12d  795  dn1dc  963  xorbi2d  1400  eueq2dc  2946  r19.44mv  3555  rexprg  3685  rextpg  3687  exmidsssn  4246  exmidsssnc  4247  swopolem  4352  sowlin  4367  elsucg  4451  elsuc2g  4452  ordsoexmid  4610  poleloe  5082  funopsn  5762  isosolem  5893  freceq2  6479  brdifun  6647  pitric  7434  elinp  7587  prloc  7604  ltexprlemloc  7720  suplocexprlemloc  7834  ltsosr  7877  aptisr  7892  suplocsrlemb  7919  axpre-ltwlin  7996  axpre-suploclemres  8014  axpre-suploc  8015  gt0add  8646  apreap  8660  apreim  8676  elznn0  9387  elznn  9388  peano2z  9408  zindd  9491  elfzp1  10194  fzm1  10222  fzosplitsni  10364  cjap  11217  dvdslelemd  12154  zeo5  12199  lcmval  12385  lcmneg  12396  lcmass  12407  isprm6  12469  infpn2  12827  lringuplu  13958  domneq0  14034  znidom  14419  dedekindeulemloc  15091  dedekindeulemeu  15094  suplociccreex  15096  dedekindicclemloc  15100  dedekindicclemeu  15103  bj-charfunr  15746  bj-nn0sucALT  15914