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

Theorem orbi12d 709
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
bi12d.1
bi12d.2
Assertion
Ref Expression
orbi12d

Proof of Theorem orbi12d
StepHypRef Expression
1 bi12d.1 . . 3
21orbi1d 702 . 2
3 bi12d.2 . . 3
43orbi2d 701 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368
This theorem is referenced by:  pm4.39  871  3orbi123d  1298  cadbi123d  1450  eueq3  3274  sbcor  3372  sbcorgOLD  3373  unjust  3479  elun  3644  elprg  4045  eltpg  4071  rabsnifsb  4098  rabrsn  4100  preq12bg  4209  disji2  4439  disjprg  4448  disjxun  4450  opthneg  4731  swopolem  4814  sotrieq  4832  isso2i  4837  somin1  5408  fununi  5659  unpreima  6013  ordsucun  6660  funcnvuni  6753  fun11iun  6760  frxp  6910  xporderlem  6911  poxp  6912  fnwelem  6915  fnse  6917  oacan  7216  omword  7238  oeword  7258  oeoa  7265  qsdisj  7407  wemapso2OLD  7998  wemapso2lem  7999  brwdom  8014  cantnflem1  8129  cantnflem1OLD  8152  r0weon  8411  infxpen  8413  sornom  8678  fin1ai  8694  isfin5  8700  isfin6  8701  sdom2en01  8703  enfin2i  8722  enfin1ai  8785  isfin5-2  8792  fin1a2lem7  8807  fin1a2lem11  8811  fin1a2lem13  8813  axdc3lem2  8852  engch  9027  eltskg  9149  tsken  9153  ltsonq  9368  addcanpr  9445  ltsosr  9492  axpre-lttri  9563  lemul1  10419  mulge0b  10437  mulle0b  10438  mulsuble0b  10439  nn1m1nn  10581  avgle  10805  nn0sub  10871  elznn0  10904  elz2  10906  nneo  10971  uztric  11131  ltxr  11353  xrrebnd  11398  xmulval  11453  xmulneg1  11490  ixxun  11574  iccsplit  11682  fzsplit2  11739  uzsplit  11779  fzospliti  11857  fzouzsplit  11860  sqeqor  12282  sumeq1  13511  sumeq2w  13514  sumeq2ii  13515  fz1f1o  13532  summo  13539  fsum  13542  prodeq1f  13715  prodeq2w  13719  prodeq2ii  13720  prodmo  13743  fprod  13748  ruclem12  13974  odd2np1lem  14045  dvdsprime  14230  coprm  14241  vdwapun  14492  vdwlem6  14504  vdwlem10  14508  mreexexlemd  15041  mreexexd  15045  istos  15665  tosso  15666  tsrlin  15849  tsrss  15853  isdomn  17943  prmirredlem  18523  prmirredlemOLD  18526  domnchr  18569  zntoslem  18595  znfld  18599  fctop  19505  cctop  19507  ppttop  19508  pptbas  19509  isufil  20404  ufilss  20406  fixufil  20423  fin1aufil  20433  xpsdsval  20884  nlmmul0or  21192  pmltpclem1  21860  iundisj2  21959  mbfmax  22056  dvne0  22412  fta1glem2  22567  plymul0or  22677  ofmulrt  22678  quotval  22688  plydivlem3  22691  plydivlem4  22692  plydivex  22693  plydivalg  22695  quotlem  22696  aalioulem2  22729  quad2  23170  dcubic2  23175  dcubic  23177  dquartlem1  23182  dquart  23184  quart  23192  leibpilem2  23272  wilthlem1  23342  muval2  23408  perfectlem2  23505  lgslem1  23571  pntpbnd1  23771  legtrid  23978  legso  23985  ishlg  23986  symquadlem  24066  islmib  24153  brbtwn2  24208  axcontlem2  24268  axcontlem4  24270  axcontlem11  24277  nb3graprlem2  24452  hashecclwwlkn1  24834  frgra2v  24999  h1datom  26500  atss  27265  atom1d  27272  atord  27307  chirred  27314  elimifd  27421  disji2f  27438  disjif2  27442  disjxpin  27447  iundisj2f  27449  disjunsn  27453  mul2lt0bi  27569  fzsplit3  27599  iundisj2fi  27602  resstos  27648  tleile  27649  trleile  27654  fsumcvg4  27932  erdsze2lem2  28648  funpsstri  29195  soseq  29334  seglelin  29766  lineunray  29797  mblfinlem2  30052  itg2addnclem2  30067  iblabsnclem  30078  ftc1anclem5  30094  fdc1  30239  unichnidl  30428  ispridl  30431  maxidlmax  30440  lzunuz  30701  dvdsrabdioph  30743  acongeq12d  30917  jm2.25  30941  rmydioph  30956  expdioph  30965  fnwe2val  30995  aomclem8  31007  unima  31441  lindslinindsimp2lem5  33063  ldepspr  33074  lcvexchlem4  34762  lcvexchlem5  34763  2at0mat0  35249  pmapjoin  35576  cdlemg17h  36394  dihlspsnat  37060
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