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

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

Proof of Theorem orbi1d
StepHypRef Expression
1 bid.1 . . 3
21orbi2d 701 . 2
3 orcom 387 . 2
4 orcom 387 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368
This theorem is referenced by:  orbi1  705  orbi12d  709  eueq2  3273  uneq1  3650  r19.45zv  3926  rexprg  4079  rextpg  4081  swopolem  4814  ordsseleq  4912  cantnflem1  8129  cantnflem1OLD  8152  axgroth2  9224  axgroth3  9230  lelttric  9712  ltxr  11353  xmulneg1  11490  fzpr  11764  elfzp12  11786  caubnd  13191  isprm6  14250  vdwlem10  14508  irredmul  17358  domneq0  17946  opsrval  18139  znfld  18599  logreclem  23150  perfectlem2  23505  legov3  23984  colperpex  24107  lmif  24151  islmib  24153  friendshipgt3  25121  h1datom  26500  xrlelttric  27572  tlt3  27653  esumpcvgval  28084  sibfof  28282  nofulllem5  29466  segcon2  29755  cnambfre  30063  pridl  30434  ismaxidl  30437  ispridlc  30467  pridlc  30468  dmnnzd  30472  lcmval  31198  lcmass  31218  fourierdlem80  31969  lindslinindsimp2  33064  sbc3orgOLD  33303  4atlem3a  35321  pmapjoin  35576  lcfl3  37221  lcfl4N  37222
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