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

Theorem orbi12d 912
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 910 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 909 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 280 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wo 841
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 208  df-or 842
This theorem is referenced by:  pm4.39  970  ifpbi123d  1069  3orbi123d  1426  cadbi123d  1602  eueq3  3701  sbcor  3821  unjust  3939  elun  4124  elprg  4580  eltpg  4617  reuprg0  4632  rabsnifsb  4652  rabrsn  4654  preq12bg  4778  disji2  5040  disjprgw  5053  disjprg  5054  disjxun  5056  swopolem  5477  sotrieq  5496  isso2i  5502  dmopab2rex  5780  somin1  5987  ordequn  6285  fununi  6423  unima  6733  unpreima  6826  ordsucun  7528  funcnvuni  7624  fiunlemw  7631  fiunlem  7634  frxp  7811  xporderlem  7812  poxp  7813  fnwelem  7816  fnse  7818  oacan  8164  omword  8186  oeword  8206  oeoa  8213  qsdisj  8364  wemapso2lem  9005  brwdom  9020  cantnflem1  9141  r0weon  9427  infxpen  9429  sornom  9688  fin1ai  9704  isfin5  9710  isfin6  9711  sdom2en01  9713  enfin2i  9732  enfin1ai  9795  isfin5-2  9802  fin1a2lem7  9817  fin1a2lem11  9821  fin1a2lem13  9823  axdc3lem2  9862  engch  10039  eltskg  10161  tsken  10165  ltsonq  10380  addcanpr  10457  ltsosr  10505  axpre-lttri  10576  lemul1  11481  mulge0b  11499  mulle0b  11500  mulsuble0b  11501  nn1m1nn  11647  avgle  11868  nn0sub  11936  elznn0  11985  elz2  11988  nneo  12055  uztric  12255  mul2lt0bi  12485  ltxr  12500  xrrebnd  12551  xmulval  12608  xmulneg1  12652  ixxun  12744  iccsplit  12861  fzsplit2  12922  uzsplit  12969  nelfzo  13033  fzospliti  13059  fzouzsplit  13062  sqeqor  13568  swrdnd  14006  sumeq1  15035  sumeq2w  15039  sumeq2ii  15040  fz1f1o  15057  summo  15064  fsum  15067  prodeq1f  15252  prodeq2w  15256  prodeq2ii  15257  prodmo  15280  fprod  15285  ruclem12  15584  odd2np1lem  15679  dvdsprime  16021  coprm  16045  vdwapun  16300  vdwlem6  16312  vdwlem10  16316  mreexexlemd  16905  mreexexd  16909  istos  17635  tosso  17636  tsrlin  17819  tsrss  17823  isdomn  19997  prmirredlem  20570  domnchr  20609  zntoslem  20633  znfld  20637  fctop  21542  cctop  21544  ppttop  21545  pptbas  21546  isufil  22441  ufilss  22443  fixufil  22460  fin1aufil  22470  xpsdsval  22920  nlmmul0or  23221  pmltpclem1  23978  iundisj2  24079  mbfmax  24179  dvne0  24537  fta1glem2  24689  plymul0or  24799  ofmulrt  24800  quotval  24810  plydivlem3  24813  plydivlem4  24814  plydivex  24815  plydivalg  24817  quotlem  24818  aalioulem2  24851  quad2  25344  dcubic2  25349  dcubic  25351  dquartlem1  25356  dquart  25358  quart  25366  leibpilem2  25447  wilthlem1  25573  muval2  25639  perfectlem2  25734  lgslem1  25801  pntpbnd1  26090  legtrid  26305  legso  26313  ishlg  26316  lnhl  26329  symquadlem  26403  islmib  26501  isinag  26552  isinagd  26553  inaghl  26559  brbtwn2  26619  axcontlem2  26679  axcontlem4  26681  axcontlem11  26688  edglnl  26856  nb3grprlem2  27091  hashecclwwlkn1  27784  nfrgr2v  27979  h1datom  29287  atss  30051  atom1d  30058  atord  30093  chirred  30100  elimifd  30226  disji2f  30256  disjif2  30260  disjxpin  30267  iundisj2f  30269  disjunsn  30273  brprop  30360  fzsplit3  30444  iundisj2fi  30447  f1ocnt  30452  resstos  30575  tleile  30576  trleile  30581  isprmidl  30875  qsidomlem1  30883  qsidomlem2  30884  smatrcl  30961  fsumcvg4  31093  erdsze2lem2  32349  satf  32498  satfv1  32508  satfbrsuc  32511  satfrnmapom  32515  satf0op  32522  sat1el2xp  32524  fmlafvel  32530  fmlasuc  32531  fmla1  32532  isfmlasuc  32533  fmlaomn0  32535  fmlasucdisj  32544  satffunlem1lem1  32547  satffunlem1lem2  32548  satffunlem2lem1  32549  dmopab3rexdif  32550  satffunlem2lem2  32551  satfv1fvfmla1  32568  2goelgoanfmla1  32569  satefvfmla1  32570  eqfunresadj  32902  funpsstri  32906  soseq  32994  seglelin  33475  lineunray  33506  topdifinffinlem  34511  topdifinffin  34512  topdifinfeq  34514  mblfinlem2  34812  itg2addnclem2  34826  iblabsnclem  34837  ftc1anclem5  34853  fdc1  34904  unichnidl  35192  ispridl  35195  maxidlmax  35204  qsdisjALTV  35732  lcvexchlem4  36055  lcvexchlem5  36056  2at0mat0  36543  pmapjoin  36870  cdlemg17h  37686  dihlspsnat  38351  lzunuz  39245  dvdsrabdioph  39287  acongeq12d  39456  jm2.25  39476  rmydioph  39491  expdioph  39500  fnwe2val  39529  aomclem8  39541  brfvrcld2  39917  uneqsn  40253  ntrneixb  40325  ntrneix3  40327  ntrneix13  40329  disjinfi  41334  salexct  42498  salexct2  42503  salexct3  42506  salgencntex  42507  salgensscntex  42508  nnfoctbdjlem  42618  nnfoctbdj  42619  iundjiun  42623  opprb  43147  euoreqb  43189  el1fzopredsuc  43406  iccpartgel  43436  paireqne  43520  divgcdoddALTV  43694  perfectALTVlem2  43734  lindslinindsimp2lem5  44415  ldepspr  44426  rrx2pnedifcoorneor  44601  rrx2plord  44605  rrx2plordisom  44608  itsclc0yqsol  44649
  Copyright terms: Public domain W3C validator