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  2946  uneq1  3320  r19.45mv  3554  rexprg  3685  rextpg  3687  swopolem  4352  sowlin  4367  onsucelsucexmidlem1  4576  onsucelsucexmid  4578  ordsoexmid  4610  isosolem  5893  acexmidlema  5935  acexmidlemb  5936  acexmidlem2  5941  acexmidlemv  5942  freceq1  6478  exmidaclem  7320  exmidac  7321  elinp  7587  prloc  7604  suplocexprlemloc  7834  ltsosr  7877  suplocsrlemb  7919  axpre-ltwlin  7996  axpre-suploclemres  8014  axpre-suploc  8015  apreap  8660  apreim  8676  sup3exmid  9030  nn01to3  9738  ltxr  9897  fzpr  10199  elfzp12  10221  lcmval  12385  lcmass  12407  isprm6  12469  lringuplu  13958  domneq0  14034  znidom  14419  dedekindeulemloc  15091  dedekindeulemeu  15094  suplociccreex  15096  dedekindicclemloc  15100  dedekindicclemeu  15103  perfectlem2  15472