Theorem orbi1d 792

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  793  orbi12d  794  xorbi1d  1392  eueq2dc  2933  uneq1  3306  r19.45mv  3540  rexprg  3670  rextpg  3672  swopolem  4336  sowlin  4351  onsucelsucexmidlem1  4560  onsucelsucexmid  4562  ordsoexmid  4594  isosolem  5867  acexmidlema  5909  acexmidlemb  5910  acexmidlem2  5915  acexmidlemv  5916  freceq1  6445  exmidaclem  7268  exmidac  7269  elinp  7534  prloc  7551  suplocexprlemloc  7781  ltsosr  7824  suplocsrlemb  7866  axpre-ltwlin  7943  axpre-suploclemres  7961  axpre-suploc  7962  apreap  8606  apreim  8622  sup3exmid  8976  nn01to3  9682  ltxr  9841  fzpr  10143  elfzp12  10165  lcmval  12201  lcmass  12223  isprm6  12285  lringuplu  13692  domneq0  13768  znidom  14145  dedekindeulemloc  14773  dedekindeulemeu  14776  suplociccreex  14778  dedekindicclemloc  14782  dedekindicclemeu  14785