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

Theorem orbi2d 764
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
orbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
orbi2d  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )

Proof of Theorem orbi2d
StepHypRef Expression
1 orbid.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 143 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32orim2d 762 . 2  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
41biimprd 157 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
54orim2d 762 . 2  |-  ( ph  ->  ( ( th  \/  ch )  ->  ( th  \/  ps ) ) )
63, 5impbid 128 1  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    \/ wo 682
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 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1d  765  orbi12d  767  dn1dc  929  xorbi2d  1343  eueq2dc  2830  r19.44mv  3427  rexprg  3545  rextpg  3547  exmidsssn  4095  exmidsssnc  4096  swopolem  4197  sowlin  4212  elsucg  4296  elsuc2g  4297  ordsoexmid  4447  poleloe  4908  isosolem  5693  freceq2  6258  brdifun  6424  pitric  7097  elinp  7250  prloc  7267  ltexprlemloc  7383  suplocexprlemloc  7497  ltsosr  7540  aptisr  7555  suplocsrlemb  7582  axpre-ltwlin  7659  axpre-suploclemres  7677  axpre-suploc  7678  gt0add  8302  apreap  8316  apreim  8332  elznn0  9027  elznn  9028  peano2z  9048  zindd  9127  elfzp1  9807  fzm1  9835  fzosplitsni  9967  cjap  10633  dvdslelemd  11453  zeo5  11497  lcmval  11656  lcmneg  11667  lcmass  11678  isprm6  11737  dedekindeulemloc  12677  dedekindeulemeu  12680  suplociccreex  12682  dedekindicclemloc  12686  dedekindicclemeu  12689  bj-nn0sucALT  13072
  Copyright terms: Public domain W3C validator