Theorem orbi1d 737

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

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

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 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1  738  orbi12d  739  xorbi1d  1312  eueq2dc  2765  uneq1  3119  r19.45mv  3335  rexprg  3444  rextpg  3446  swopolem  4060  sowlin  4075  onsucelsucexmidlem1  4271  onsucelsucexmid  4273  ordsoexmid  4305  isosolem  5483  acexmidlema  5523  acexmidlemb  5524  acexmidlem2  5529  acexmidlemv  5530  freceq1  6002  elinp  6664  prloc  6681  ltsosr  6941  axpre-ltwlin  7049  apreap  7687  apreim  7703  nn01to3  8702  ltxr  8849  fzpr  9094  elfzp12  9116  lcmval  10445  lcmass  10467  isprm6  10526