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

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
StepHypRef Expression
1 orbid.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21orbi2d 739 . 2  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
3 orcom 682 . 2  |-  ( ( ps  \/  th )  <->  ( th  \/  ps )
)
4 orcom 682 . 2  |-  ( ( ch  \/  th )  <->  ( th  \/  ch )
)
52, 3, 43bitr4g 221 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator