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

Theorem orbi2i 734
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 733 . 2  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
41biimpri 132 . . 3  |-  ( ps 
->  ph )
54orim2i 733 . 2  |-  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) )
63, 5impbii 125 1  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 680
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 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  orbi1i  735  orbi12i  736  orass  739  or4  743  or42  744  orordir  746  dcnnOLD  817  orbididc  920  3orcomb  954  excxor  1339  xordc  1353  nf4dc  1631  nf4r  1632  19.44  1643  dveeq2  1769  dvelimALT  1961  dvelimfv  1962  dvelimor  1969  dcne  2294  unass  3201  undi  3292  undif3ss  3305  symdifxor  3310  undif4  3393  iinuniss  3863  ordsucim  4384  suc11g  4440  qfto  4896  nntri3or  6355  reapcotr  8323  elnn0  8930  elxnn0  8993  elnn1uz2  9350  nn01to3  9358  elxr  9503  xaddcom  9584  xnegdi  9591  xpncan  9594  xleadd1a  9596  lcmdvds  11656  mulgcddvds  11671  cncongr2  11681  bj-peano4  12964
  Copyright terms: Public domain W3C validator