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

Theorem orbi2d 737
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 142 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32orim2d 735 . 2  |-  ( ph  ->  ( ( th  \/  ps )  ->  ( th  \/  ch ) ) )
41biimprd 156 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
54orim2d 735 . 2  |-  ( ph  ->  ( ( th  \/  ch )  ->  ( th  \/  ps ) ) )
63, 5impbid 127 1  |-  ( ph  ->  ( ( th  \/  ps )  <->  ( th  \/  ch ) ) )
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:  orbi1d  738  orbi12d  740  dn1dc  902  xorbi2d  1312  eueq2dc  2774  r19.44mv  3352  rexprg  3462  rextpg  3464  swopolem  4088  sowlin  4103  elsucg  4187  elsuc2g  4188  ordsoexmid  4333  poleloe  4774  isosolem  5514  freceq2  6062  brdifun  6220  pitric  6625  elinp  6778  prloc  6795  ltexprlemloc  6911  ltsosr  7055  aptisr  7069  axpre-ltwlin  7163  gt0add  7792  apreap  7806  apreim  7822  elznn0  8499  elznn  8500  peano2z  8520  zindd  8598  elfzp1  9217  fzm1  9245  fzosplitsni  9373  cjap  9994  dvdslelemd  10451  zeo5  10495  lcmval  10652  lcmneg  10663  lcmass  10674  isprm6  10733  bj-nn0sucALT  11040
  Copyright terms: Public domain W3C validator