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 ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi1  804  orbi12d  805  xorbi1d  1430  eueq2dc  2999  uneq1  3376  r19.45mv  3621  rexprg  3761  rextpg  3763  swopolem  4450  sowlin  4465  onsucelsucexmidlem1  4675  onsucelsucexmid  4677  ordsoexmid  4709  isosolem  6030  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  acexmidlemv  6083  freceq1  6663  exmidaclem  7564  exmidac  7565  papcotr  7613  elinp  7841  prloc  7858  suplocexprlemloc  8088  ltsosr  8131  suplocsrlemb  8173  axpre-ltwlin  8250  axpre-suploclemres  8268  axpre-suploc  8269  apreap  8915  apreim  8931  sup3exmid  9287  nn01to3  10017  ltxr  10177  fzpr  10484  elfzp12  10506  lcmval  12841  lcmass  12863  isprm6  12925  ballotfilemfc0  13232  ballotfilemfcc  13233  lringuplu  14503  domneq0  14581  znidom  14992  dedekindeulemloc  15720  dedekindeulemeu  15723  suplociccreex  15725  dedekindicclemloc  15729  dedekindicclemeu  15732  perfectlem2  16114