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  2953  uneq1  3328  r19.45mv  3562  rexprg  3695  rextpg  3697  swopolem  4370  sowlin  4385  onsucelsucexmidlem1  4594  onsucelsucexmid  4596  ordsoexmid  4628  isosolem  5916  acexmidlema  5958  acexmidlemb  5959  acexmidlem2  5964  acexmidlemv  5965  freceq1  6501  exmidaclem  7351  exmidac  7352  elinp  7622  prloc  7639  suplocexprlemloc  7869  ltsosr  7912  suplocsrlemb  7954  axpre-ltwlin  8031  axpre-suploclemres  8049  axpre-suploc  8050  apreap  8695  apreim  8711  sup3exmid  9065  nn01to3  9773  ltxr  9932  fzpr  10234  elfzp12  10256  lcmval  12500  lcmass  12522  isprm6  12584  lringuplu  14073  domneq0  14149  znidom  14534  dedekindeulemloc  15206  dedekindeulemeu  15209  suplociccreex  15211  dedekindicclemloc  15215  dedekindicclemeu  15218  perfectlem2  15587