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

Theorem orbi2i 736
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 119 . . 3  |-  ( ph  ->  ps )
32orim2i 735 . 2  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
41biimpri 132 . . 3  |-  ( ps 
->  ph )
54orim2i 735 . 2  |-  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) )
63, 5impbii 125 1  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> 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:  orbi1i  737  orbi12i  738  orass  741  or4  745  or42  746  orordir  748  dcnnOLD  819  orbididc  922  3orcomb  956  excxor  1341  xordc  1355  nf4dc  1633  nf4r  1634  19.44  1645  dveeq2  1771  dvelimALT  1963  dvelimfv  1964  dvelimor  1971  dcne  2296  unass  3203  undi  3294  undif3ss  3307  symdifxor  3312  undif4  3395  iinuniss  3865  ordsucim  4386  suc11g  4442  qfto  4898  nntri3or  6357  reapcotr  8328  elnn0  8947  elxnn0  9010  elnn1uz2  9369  nn01to3  9377  elxr  9531  xaddcom  9612  xnegdi  9619  xpncan  9622  xleadd1a  9624  lcmdvds  11687  mulgcddvds  11702  cncongr2  11712  bj-peano4  13080
  Copyright terms: Public domain W3C validator