Theorem orbi1d 796

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  797  orbi12d  798  xorbi1d  1423  eueq2dc  2976  uneq1  3351  r19.45mv  3585  rexprg  3718  rextpg  3720  swopolem  4396  sowlin  4411  onsucelsucexmidlem1  4620  onsucelsucexmid  4622  ordsoexmid  4654  isosolem  5948  acexmidlema  5992  acexmidlemb  5993  acexmidlem2  5998  acexmidlemv  5999  freceq1  6538  exmidaclem  7390  exmidac  7391  elinp  7661  prloc  7678  suplocexprlemloc  7908  ltsosr  7951  suplocsrlemb  7993  axpre-ltwlin  8070  axpre-suploclemres  8088  axpre-suploc  8089  apreap  8734  apreim  8750  sup3exmid  9104  nn01to3  9812  ltxr  9971  fzpr  10273  elfzp12  10295  lcmval  12585  lcmass  12607  isprm6  12669  lringuplu  14160  domneq0  14236  znidom  14621  dedekindeulemloc  15293  dedekindeulemeu  15296  suplociccreex  15298  dedekindicclemloc  15302  dedekindicclemeu  15305  perfectlem2  15674