Theorem orbi1d 799

Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
orbid.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
orbi1d	|- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )

Proof of Theorem orbi1d

Step	Hyp	Ref	Expression
1		orbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	orbi2d 798	. 2 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )
3		orcom 736	. 2 |- ( ( ps \/ th ) <-> ( th \/ ps ) )
4		orcom 736	. 2 |- ( ( ch \/ th ) <-> ( th \/ ch ) )
5	2, 3, 4	3bitr4g 223	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )

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:  orbi1  800  orbi12d  801  xorbi1d  1426  eueq2dc  2980  uneq1  3356  r19.45mv  3590  rexprg  3725  rextpg  3727  swopolem  4408  sowlin  4423  onsucelsucexmidlem1  4632  onsucelsucexmid  4634  ordsoexmid  4666  isosolem  5975  acexmidlema  6019  acexmidlemb  6020  acexmidlem2  6025  acexmidlemv  6026  freceq1  6601  exmidaclem  7483  exmidac  7484  elinp  7754  prloc  7771  suplocexprlemloc  8001  ltsosr  8044  suplocsrlemb  8086  axpre-ltwlin  8163  axpre-suploclemres  8181  axpre-suploc  8182  apreap  8826  apreim  8842  sup3exmid  9196  nn01to3  9912  ltxr  10071  fzpr  10374  elfzp12  10396  lcmval  12715  lcmass  12737  isprm6  12799  lringuplu  14291  domneq0  14368  znidom  14753  dedekindeulemloc  15430  dedekindeulemeu  15433  suplociccreex  15435  dedekindicclemloc  15439  dedekindicclemeu  15442  perfectlem2  15814