Theorem orbi1d 740

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

Syntax hints:   -> wi 4   <-> wb 103   \/ wo 664

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1  741  orbi12d  742  xorbi1d  1317  eueq2dc  2788  uneq1  3147  r19.45mv  3375  rexprg  3494  rextpg  3496  swopolem  4132  sowlin  4147  onsucelsucexmidlem1  4344  onsucelsucexmid  4346  ordsoexmid  4378  isosolem  5603  acexmidlema  5643  acexmidlemb  5644  acexmidlem2  5649  acexmidlemv  5650  freceq1  6157  elinp  7031  prloc  7048  ltsosr  7308  axpre-ltwlin  7416  apreap  8062  apreim  8078  nn01to3  9100  ltxr  9244  fzpr  9487  elfzp12  9509  lcmval  11319  lcmass  11341  isprm6  11400