MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orbi2d Unicode version

Theorem orbi2d 701
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
bid.1
Assertion
Ref Expression
orbi2d

Proof of Theorem orbi2d
StepHypRef Expression
1 bid.1 . . 3
21imbi2d 316 . 2
3 df-or 370 . 2
4 df-or 370 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368
This theorem is referenced by:  orbi1d  702  orbi12d  709  cad1  1465  eueq2  3273  sbc2or  3336  r19.44zv  3927  rexprg  4079  rextpg  4081  swopolem  4814  elsucg  4950  elsuc2g  4951  poleloe  5406  brdifun  7357  brwdom  8014  isfin1a  8693  elgch  9021  suplem2pr  9452  axlttri  9677  mulcan1g  10227  elznn0  10904  elznn  10905  zindd  10990  rpneg  11278  dfle2  11382  fzm1  11787  fzosplitsni  11920  hashv01gt1  12418  bitsf1  14096  isprm6  14250  infpn2  14431  irredmul  17358  domneq0  17946  znfld  18599  quotval  22688  plydivlem4  22692  plydivex  22693  aalioulem2  22729  aalioulem5  22732  aalioulem6  22733  aaliou  22734  aaliou2  22736  aaliou2b  22737  axcontlem7  24273  hashecclwwlkn1  24834  eliccioo  27627  tlt2  27652  sibfof  28282  ballotlemfc0  28431  ballotlemfcc  28432  seglelin  29766  lineunray  29797  mblfinlem2  30052  pridl  30434  maxidlval  30436  ispridlc  30467  pridlc  30468  dmnnzd  30472  aomclem8  31007  lcmval  31198  lcmneg  31209  lcmass  31218  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  orbi1r  33279  lcfl7N  37228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
  Copyright terms: Public domain W3C validator