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

Theorem orbi2d 704
 Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
orbid.1
Assertion
Ref Expression
orbi2d

Proof of Theorem orbi2d
StepHypRef Expression
1 orbid.1 . . . 4
21biimpd 132 . . 3
32orim2d 702 . 2
41biimprd 147 . . 3
54orim2d 702 . 2
63, 5impbid 120 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 98   wo 629 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  orbi1d  705  orbi12d  707  dn1dc  867  xorbi2d  1271  eueq2dc  2714  rexprg  3422  rextpg  3424  swopolem  4042  sowlin  4057  elsucg  4141  elsuc2g  4142  ordsoexmid  4286  poleloe  4724  isosolem  5463  freceq2  5980  brdifun  6133  pitric  6419  elinp  6572  prloc  6589  ltexprlemloc  6705  ltsosr  6849  aptisr  6863  axpre-ltwlin  6957  gt0add  7564  apreap  7578  apreim  7594  elznn0  8260  elznn  8261  peano2z  8281  zindd  8356  elfzp1  8934  fzm1  8962  fzosplitsni  9091  cjap  9506  bj-nn0sucALT  10103
 Copyright terms: Public domain W3C validator