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  2934  uneq1  3307  r19.45mv  3541  rexprg  3671  rextpg  3673  swopolem  4337  sowlin  4352  onsucelsucexmidlem1  4561  onsucelsucexmid  4563  ordsoexmid  4595  isosolem  5868  acexmidlema  5910  acexmidlemb  5911  acexmidlem2  5916  acexmidlemv  5917  freceq1  6447  exmidaclem  7270  exmidac  7271  elinp  7536  prloc  7553  suplocexprlemloc  7783  ltsosr  7826  suplocsrlemb  7868  axpre-ltwlin  7945  axpre-suploclemres  7963  axpre-suploc  7964  apreap  8608  apreim  8624  sup3exmid  8978  nn01to3  9685  ltxr  9844  fzpr  10146  elfzp12  10168  lcmval  12204  lcmass  12226  isprm6  12288  lringuplu  13695  domneq0  13771  znidom  14156  dedekindeulemloc  14798  dedekindeulemeu  14801  suplociccreex  14803  dedekindicclemloc  14807  dedekindicclemeu  14810