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  2993  uneq1  3370  r19.45mv  3607  rexprg  3746  rextpg  3748  swopolem  4431  sowlin  4446  onsucelsucexmidlem1  4655  onsucelsucexmid  4657  ordsoexmid  4689  isosolem  6003  acexmidlema  6049  acexmidlemb  6050  acexmidlem2  6055  acexmidlemv  6056  freceq1  6636  exmidaclem  7528  exmidac  7529  papcotr  7577  elinp  7805  prloc  7822  suplocexprlemloc  8052  ltsosr  8095  suplocsrlemb  8137  axpre-ltwlin  8214  axpre-suploclemres  8232  axpre-suploc  8233  apreap  8878  apreim  8894  sup3exmid  9248  nn01to3  9967  ltxr  10127  fzpr  10433  elfzp12  10455  lcmval  12785  lcmass  12807  isprm6  12869  ballotfilemfc0  13176  ballotfilemfcc  13177  lringuplu  14441  domneq0  14519  znidom  14931  dedekindeulemloc  15610  dedekindeulemeu  15613  suplociccreex  15615  dedekindicclemloc  15619  dedekindicclemeu  15622  perfectlem2  15994