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

Theorem orbi2i 714
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 118 . . 3  |-  ( ph  ->  ps )
32orim2i 713 . 2  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
41biimpri 131 . . 3  |-  ( ps 
->  ph )
54orim2i 713 . 2  |-  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) )
63, 5impbii 124 1  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> 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:  orbi1i  715  orbi12i  716  orass  719  or4  723  or42  724  orordir  726  testbitestn  861  orbididc  899  3orcomb  933  excxor  1314  xordc  1328  nf4dc  1605  nf4r  1606  19.44  1617  dveeq2  1743  dvelimALT  1934  dvelimfv  1935  dvelimor  1942  dcne  2266  unass  3155  undi  3245  undif3ss  3258  symdifxor  3263  undif4  3342  iinuniss  3806  ordsucim  4307  suc11g  4363  qfto  4808  nntri3or  6236  reapcotr  8051  elnn0  8645  elxnn0  8708  elnn1uz2  9063  nn01to3  9071  elxr  9216  lcmdvds  11143  mulgcddvds  11158  cncongr2  11168  bj-peano4  11496
  Copyright terms: Public domain W3C validator