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  2937  uneq1  3311  r19.45mv  3545  rexprg  3675  rextpg  3677  swopolem  4341  sowlin  4356  onsucelsucexmidlem1  4565  onsucelsucexmid  4567  ordsoexmid  4599  isosolem  5874  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  acexmidlemv  5923  freceq1  6459  exmidaclem  7291  exmidac  7292  elinp  7558  prloc  7575  suplocexprlemloc  7805  ltsosr  7848  suplocsrlemb  7890  axpre-ltwlin  7967  axpre-suploclemres  7985  axpre-suploc  7986  apreap  8631  apreim  8647  sup3exmid  9001  nn01to3  9708  ltxr  9867  fzpr  10169  elfzp12  10191  lcmval  12256  lcmass  12278  isprm6  12340  lringuplu  13828  domneq0  13904  znidom  14289  dedekindeulemloc  14939  dedekindeulemeu  14942  suplociccreex  14944  dedekindicclemloc  14948  dedekindicclemeu  14951  perfectlem2  15320