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

Theorem orbi1d 738
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 737 . 2  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
3 orcom 680 . 2  |-  ( ( ps  \/  th )  <->  ( th  \/  ps )
)
4 orcom 680 . 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 662
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 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  orbi1  739  orbi12d  740  xorbi1d  1313  eueq2dc  2774  uneq1  3129  r19.45mv  3351  rexprg  3462  rextpg  3464  swopolem  4088  sowlin  4103  onsucelsucexmidlem1  4299  onsucelsucexmid  4301  ordsoexmid  4333  isosolem  5514  acexmidlema  5554  acexmidlemb  5555  acexmidlem2  5560  acexmidlemv  5561  freceq1  6061  elinp  6778  prloc  6795  ltsosr  7055  axpre-ltwlin  7163  apreap  7806  apreim  7822  nn01to3  8835  ltxr  8979  fzpr  9222  elfzp12  9244  lcmval  10652  lcmass  10674  isprm6  10733
  Copyright terms: Public domain W3C validator