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  4247  exmidsssnc  4248  swopolem  4353  sowlin  4368  elsucg  4452  elsuc2g  4453  ordsoexmid  4611  poleloe  5083  funopsn  5764  isosolem  5895  freceq2  6481  brdifun  6649  pitric  7436  elinp  7589  prloc  7606  ltexprlemloc  7722  suplocexprlemloc  7836  ltsosr  7879  aptisr  7894  suplocsrlemb  7921  axpre-ltwlin  7998  axpre-suploclemres  8016  axpre-suploc  8017  gt0add  8648  apreap  8662  apreim  8678  elznn0  9389  elznn  9390  peano2z  9410  zindd  9493  elfzp1  10196  fzm1  10224  fzosplitsni  10366  cjap  11250  dvdslelemd  12187  zeo5  12232  lcmval  12418  lcmneg  12429  lcmass  12440  isprm6  12502  infpn2  12860  lringuplu  13991  domneq0  14067  znidom  14452  dedekindeulemloc  15124  dedekindeulemeu  15127  suplociccreex  15129  dedekindicclemloc  15133  dedekindicclemeu  15136  bj-charfunr  15783  bj-nn0sucALT  15951