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

Theorem orbi2i 752
 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
Assertion
Ref Expression
orbi2i

Proof of Theorem orbi2i
StepHypRef Expression
1 orbi2i.1 . . . 4
21biimpi 119 . . 3
32orim2i 751 . 2
41biimpri 132 . . 3
54orim2i 751 . 2
63, 5impbii 125 1
 Colors of variables: wff set class Syntax hints:   wb 104   wo 698 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 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  orbi1i  753  orbi12i  754  orass  757  or4  761  or42  762  orordir  764  dcnnOLD  835  orbididc  938  3orcomb  972  excxor  1360  xordc  1374  nf4dc  1650  nf4r  1651  19.44  1662  dveeq2  1795  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  dcne  2338  unass  3264  undi  3355  undif3ss  3368  symdifxor  3373  undif4  3456  iinuniss  3931  ordsucim  4458  suc11g  4515  qfto  4974  nntri3or  6437  reapcotr  8467  elnn0  9086  elxnn0  9149  elnn1uz2  9511  nn01to3  9519  elxr  9676  xaddcom  9758  xnegdi  9765  xpncan  9768  xleadd1a  9770  lcmdvds  11947  mulgcddvds  11962  cncongr2  11972  bj-peano4  13501  apdifflemr  13589
 Copyright terms: Public domain W3C validator