Theorem orbi1d 793

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 792	. 2 |- ( ph -> ( ( th \/ ps ) <-> ( th \/ ch ) ) )
3		orcom 730	. 2 |- ( ( ps \/ th ) <-> ( th \/ ps ) )
4		orcom 730	. 2 |- ( ( ch \/ th ) <-> ( th \/ ch ) )
5	2, 3, 4	3bitr4g 223	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )

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:  orbi1  794  orbi12d  795  xorbi1d  1401  eueq2dc  2946  uneq1  3320  r19.45mv  3554  rexprg  3685  rextpg  3687  swopolem  4353  sowlin  4368  onsucelsucexmidlem1  4577  onsucelsucexmid  4579  ordsoexmid  4611  isosolem  5895  acexmidlema  5937  acexmidlemb  5938  acexmidlem2  5943  acexmidlemv  5944  freceq1  6480  exmidaclem  7322  exmidac  7323  elinp  7589  prloc  7606  suplocexprlemloc  7836  ltsosr  7879  suplocsrlemb  7921  axpre-ltwlin  7998  axpre-suploclemres  8016  axpre-suploc  8017  apreap  8662  apreim  8678  sup3exmid  9032  nn01to3  9740  ltxr  9899  fzpr  10201  elfzp12  10223  lcmval  12418  lcmass  12440  isprm6  12502  lringuplu  13991  domneq0  14067  znidom  14452  dedekindeulemloc  15124  dedekindeulemeu  15127  suplociccreex  15129  dedekindicclemloc  15133  dedekindicclemeu  15136  perfectlem2  15505