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

Theorem orbi12d 741
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 734 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 733 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 266 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  pm4.39  910  ifpbi123d  1020  3orbi123d  1389  cadbi123d  1539  eueq3  3347  sbcor  3445  unjust  3543  elun  3714  elprg  4143  eltpg  4173  rabsnifsb  4200  rabrsn  4202  preq12bg  4321  disji2  4563  disjprg  4572  disjxun  4575  swopolem  4957  sotrieq  4975  isso2i  4980  somin1  5434  ordequn  5730  fununi  5863  unpreima  6233  ordsucun  6894  funcnvuni  6989  fun11iun  6996  frxp  7151  xporderlem  7152  poxp  7153  fnwelem  7156  fnse  7158  oacan  7492  omword  7514  oeword  7534  oeoa  7541  qsdisj  7688  wemapso2lem  8317  brwdom  8332  cantnflem1  8446  r0weon  8695  infxpen  8697  sornom  8959  fin1ai  8975  isfin5  8981  isfin6  8982  sdom2en01  8984  enfin2i  9003  enfin1ai  9066  isfin5-2  9073  fin1a2lem7  9088  fin1a2lem11  9092  fin1a2lem13  9094  axdc3lem2  9133  engch  9306  eltskg  9428  tsken  9432  ltsonq  9647  addcanpr  9724  ltsosr  9771  axpre-lttri  9842  lemul1  10726  mulge0b  10744  mulle0b  10745  mulsuble0b  10746  nn1m1nn  10889  avgle  11123  nn0sub  11192  elznn0  11227  elz2  11229  nneo  11295  uztric  11543  mul2lt0bi  11770  ltxr  11786  xrrebnd  11834  xmulval  11891  xmulneg1  11930  ixxun  12020  iccsplit  12134  fzsplit2  12194  uzsplit  12238  nelfzo  12301  fzospliti  12326  fzouzsplit  12329  sqeqor  12797  swrdnd  13232  sumeq1  14215  sumeq2w  14218  sumeq2ii  14219  fz1f1o  14236  summo  14243  fsum  14246  prodeq1f  14425  prodeq2w  14429  prodeq2ii  14430  prodmo  14453  fprod  14458  ruclem12  14757  odd2np1lem  14850  dvdsprime  15186  coprm  15209  vdwapun  15464  vdwlem6  15476  vdwlem10  15480  mreexexlemd  16075  mreexexd  16079  mreexexdOLD  16080  istos  16806  tosso  16807  tsrlin  16990  tsrss  16994  isdomn  19063  prmirredlem  19607  domnchr  19646  zntoslem  19671  znfld  19675  fctop  20565  cctop  20567  ppttop  20568  pptbas  20569  isufil  21464  ufilss  21466  fixufil  21483  fin1aufil  21493  xpsdsval  21943  nlmmul0or  22244  pmltpclem1  22968  iundisj2  23068  mbfmax  23166  dvne0  23522  fta1glem2  23674  plymul0or  23784  ofmulrt  23785  quotval  23795  plydivlem3  23798  plydivlem4  23799  plydivex  23800  plydivalg  23802  quotlem  23803  aalioulem2  23836  quad2  24310  dcubic2  24315  dcubic  24317  dquartlem1  24322  dquart  24324  quart  24332  leibpilem2  24412  wilthlem1  24538  muval2  24604  perfectlem2  24699  lgslem1  24766  pntpbnd1  25019  legtrid  25231  legso  25239  ishlg  25242  lnhl  25255  symquadlem  25329  islmib  25424  isinag  25474  inaghl  25476  brbtwn2  25530  axcontlem2  25590  axcontlem4  25592  axcontlem11  25599  nb3graprlem2  25774  hashecclwwlkn1  26154  frgra2v  26319  h1datom  27618  atss  28382  atom1d  28389  atord  28424  chirred  28431  elimifd  28539  disji2f  28565  disjif2  28569  disjxpin  28576  iundisj2f  28578  disjunsn  28582  fzsplit3  28733  iundisj2fi  28736  f1ocnt  28739  resstos  28784  tleile  28785  trleile  28790  smatrcl  28983  fsumcvg4  29117  erdsze2lem2  30233  funpsstri  30702  soseq  30788  seglelin  31186  lineunray  31217  topdifinffinlem  32154  topdifinffin  32155  topdifinfeq  32157  mblfinlem2  32400  itg2addnclem2  32415  iblabsnclem  32426  ftc1anclem5  32442  fdc1  32495  unichnidl  32783  ispridl  32786  maxidlmax  32795  lcvexchlem4  33125  lcvexchlem5  33126  2at0mat0  33612  pmapjoin  33939  cdlemg17h  34757  dihlspsnat  35423  lzunuz  36132  dvdsrabdioph  36175  acongeq12d  36347  jm2.25  36367  rmydioph  36382  expdioph  36391  fnwe2val  36420  aomclem8  36432  brfvrcld2  36786  uneqsn  37124  ntrneixb  37196  ntrneix3  37198  ntrneix13  37200  sbcorgOLD  37544  unima  38123  disjinfi  38158  salexct  39011  salexct2  39016  salexct3  39019  salgencntex  39020  salgensscntex  39021  nnfoctbdjlem  39131  nnfoctbdj  39132  iundjiun  39136  el1fzopredsuc  39732  iccpartgel  39751  divgcdoddALTV  39915  perfectALTVlem2  39949  nb3grprlem2  40590  hashecclwwlksn1  41242  nfrgr2v  41423  lindslinindsimp2lem5  42026  ldepspr  42037
  Copyright terms: Public domain W3C validator