Theorem orbi1d 799

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  800  orbi12d  801  xorbi1d  1426  eueq2dc  2990  uneq1  3366  r19.45mv  3603  rexprg  3741  rextpg  3743  swopolem  4426  sowlin  4441  onsucelsucexmidlem1  4650  onsucelsucexmid  4652  ordsoexmid  4684  isosolem  5997  acexmidlema  6041  acexmidlemb  6042  acexmidlem2  6047  acexmidlemv  6048  freceq1  6623  exmidaclem  7515  exmidac  7516  papcotr  7562  elinp  7789  prloc  7806  suplocexprlemloc  8036  ltsosr  8079  suplocsrlemb  8121  axpre-ltwlin  8198  axpre-suploclemres  8216  axpre-suploc  8217  apreap  8861  apreim  8877  sup3exmid  9231  nn01to3  9949  ltxr  10108  fzpr  10411  elfzp12  10433  lcmval  12760  lcmass  12782  isprm6  12844  lringuplu  14341  domneq0  14418  znidom  14805  dedekindeulemloc  15484  dedekindeulemeu  15487  suplociccreex  15489  dedekindicclemloc  15493  dedekindicclemeu  15496  perfectlem2  15868