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  4452  sowlin  4467  onsucelsucexmidlem1  4677  onsucelsucexmid  4679  ordsoexmid  4711  isosolem  6033  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  acexmidlemv  6086  freceq1  6668  exmidaclem  7570  exmidac  7571  papcotr  7619  elinp  7847  prloc  7864  suplocexprlemloc  8094  ltsosr  8137  suplocsrlemb  8179  axpre-ltwlin  8256  axpre-suploclemres  8274  axpre-suploc  8275  apreap  8923  apreim  8939  sup3exmid  9295  nn01to3  10032  ltxr  10193  fzpr  10500  elfzp12  10522  lcmval  12865  lcmass  12887  isprm6  12950  ballotfilemfc0  13289  ballotfilemfcc  13290  lringuplu  14611  domneq0  14689  znidom  15100  dedekindeulemloc  15862  dedekindeulemeu  15865  suplociccreex  15867  dedekindicclemloc  15871  dedekindicclemeu  15874  perfectlem2  16317