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

Theorem orbi2i 689
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
Hypothesis
Ref Expression
orbi2i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
orbi2i  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)

Proof of Theorem orbi2i
StepHypRef Expression
1 orbi2i.1 . . . 4  |-  ( ph  <->  ps )
21biimpi 117 . . 3  |-  ( ph  ->  ps )
32orim2i 688 . 2  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
41biimpri 128 . . 3  |-  ( ps 
->  ph )
54orim2i 688 . 2  |-  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) )
63, 5impbii 121 1  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 102    \/ wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  orbi1i  690  orbi12i  691  orass  694  or4  698  or42  699  orordir  701  testbitestn  834  orbididc  871  3orcomb  905  excxor  1285  xordc  1299  nf4dc  1576  nf4r  1577  19.44  1588  dveeq2  1712  dvelimALT  1902  dvelimfv  1903  dvelimor  1910  dcne  2231  unass  3128  undi  3213  undif3ss  3226  symdifxor  3231  undif4  3312  iinuniss  3765  ordsucim  4254  suc11g  4309  qfto  4742  nntri3or  6103  reapcotr  7663  elnn0  8241  elnn1uz2  8641  nn01to3  8649  elxr  8797  bj-peano4  10467
  Copyright terms: Public domain W3C validator