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  1371  eueq2dc  2899  uneq1  3269  r19.45mv  3502  rexprg  3628  rextpg  3630  swopolem  4283  sowlin  4298  onsucelsucexmidlem1  4505  onsucelsucexmid  4507  ordsoexmid  4539  isosolem  5792  acexmidlema  5833  acexmidlemb  5834  acexmidlem2  5839  acexmidlemv  5840  freceq1  6360  exmidaclem  7164  exmidac  7165  elinp  7415  prloc  7432  suplocexprlemloc  7662  ltsosr  7705  suplocsrlemb  7747  axpre-ltwlin  7824  axpre-suploclemres  7842  axpre-suploc  7843  apreap  8485  apreim  8501  sup3exmid  8852  nn01to3  9555  ltxr  9711  fzpr  10012  elfzp12  10034  lcmval  11995  lcmass  12017  isprm6  12079  dedekindeulemloc  13237  dedekindeulemeu  13240  suplociccreex  13242  dedekindicclemloc  13246  dedekindicclemeu  13249