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  6667  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  10033  ltxr  10194  fzpr  10501  elfzp12  10523  lcmval  12866  lcmass  12888  isprm6  12951  ballotfilemfc0  13290  ballotfilemfcc  13291  lringuplu  14612  domneq0  14690  znidom  15101  dedekindeulemloc  15845  dedekindeulemeu  15848  suplociccreex  15850  dedekindicclemloc  15854  dedekindicclemeu  15857  perfectlem2  16300