Theorem orbi1d 791

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  792  orbi12d  793  xorbi1d  1381  eueq2dc  2912  uneq1  3284  r19.45mv  3518  rexprg  3646  rextpg  3648  swopolem  4307  sowlin  4322  onsucelsucexmidlem1  4529  onsucelsucexmid  4531  ordsoexmid  4563  isosolem  5827  acexmidlema  5868  acexmidlemb  5869  acexmidlem2  5874  acexmidlemv  5875  freceq1  6395  exmidaclem  7209  exmidac  7210  elinp  7475  prloc  7492  suplocexprlemloc  7722  ltsosr  7765  suplocsrlemb  7807  axpre-ltwlin  7884  axpre-suploclemres  7902  axpre-suploc  7903  apreap  8546  apreim  8562  sup3exmid  8916  nn01to3  9619  ltxr  9777  fzpr  10079  elfzp12  10101  lcmval  12065  lcmass  12087  isprm6  12149  lringuplu  13342  dedekindeulemloc  14182  dedekindeulemeu  14185  suplociccreex  14187  dedekindicclemloc  14191  dedekindicclemeu  14194