Theorem orbi1d 803

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

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

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  804  orbi12d  805  xorbi1d  1430  eueq2dc  2999  uneq1  3376  r19.45mv  3618  rexprg  3757  rextpg  3759  swopolem  4445  sowlin  4460  onsucelsucexmidlem1  4670  onsucelsucexmid  4672  ordsoexmid  4704  isosolem  6020  acexmidlema  6066  acexmidlemb  6067  acexmidlem2  6072  acexmidlemv  6073  freceq1  6653  exmidaclem  7554  exmidac  7555  papcotr  7603  elinp  7831  prloc  7848  suplocexprlemloc  8078  ltsosr  8121  suplocsrlemb  8163  axpre-ltwlin  8240  axpre-suploclemres  8258  axpre-suploc  8259  apreap  8905  apreim  8921  sup3exmid  9277  nn01to3  9996  ltxr  10156  fzpr  10462  elfzp12  10484  lcmval  12819  lcmass  12841  isprm6  12903  ballotfilemfc0  13210  ballotfilemfcc  13211  lringuplu  14476  domneq0  14554  znidom  14964  dedekindeulemloc  15643  dedekindeulemeu  15646  suplociccreex  15648  dedekindicclemloc  15652  dedekindicclemeu  15655  perfectlem2  16028