Theorem orbi1d 781

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

Syntax hints:   -> wi 4   <-> wb 104   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1  782  orbi12d  783  xorbi1d  1360  eueq2dc  2861  uneq1  3228  r19.45mv  3461  rexprg  3583  rextpg  3585  swopolem  4235  sowlin  4250  onsucelsucexmidlem1  4451  onsucelsucexmid  4453  ordsoexmid  4485  isosolem  5733  acexmidlema  5773  acexmidlemb  5774  acexmidlem2  5779  acexmidlemv  5780  freceq1  6297  exmidaclem  7081  exmidac  7082  elinp  7306  prloc  7323  suplocexprlemloc  7553  ltsosr  7596  suplocsrlemb  7638  axpre-ltwlin  7715  axpre-suploclemres  7733  axpre-suploc  7734  apreap  8373  apreim  8389  sup3exmid  8739  nn01to3  9436  ltxr  9592  fzpr  9888  elfzp12  9910  lcmval  11780  lcmass  11802  isprm6  11861  dedekindeulemloc  12805  dedekindeulemeu  12808  suplociccreex  12810  dedekindicclemloc  12814  dedekindicclemeu  12817