ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  orbi1d Unicode version

Theorem orbi1d 763
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
StepHypRef Expression
1 orbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21orbi2d 762 . 2  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
3 orcom 700 . 2  |-  ( ( ps  \/  th )  <->  ( th  \/  ps )
)
4 orcom 700 . 2  |-  ( ( ch  \/  th )  <->  ( th  \/  ch )
)
52, 3, 43bitr4g 222 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    \/ wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1  764  orbi12d  765  xorbi1d  1342  eueq2dc  2828  uneq1  3191  r19.45mv  3424  rexprg  3543  rextpg  3545  swopolem  4195  sowlin  4210  onsucelsucexmidlem1  4411  onsucelsucexmid  4413  ordsoexmid  4445  isosolem  5691  acexmidlema  5731  acexmidlemb  5732  acexmidlem2  5737  acexmidlemv  5738  freceq1  6255  exmidaclem  7028  exmidac  7029  elinp  7246  prloc  7263  suplocexprlemloc  7493  ltsosr  7536  suplocsrlemb  7578  axpre-ltwlin  7655  axpre-suploclemres  7673  axpre-suploc  7674  apreap  8312  apreim  8328  sup3exmid  8672  nn01to3  9358  ltxr  9502  fzpr  9797  elfzp12  9819  lcmval  11640  lcmass  11662  isprm6  11721  dedekindeulemloc  12661  dedekindeulemeu  12664
  Copyright terms: Public domain W3C validator