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

Theorem orbi12d 746
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 739 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 738 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 268 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382
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 197  df-or 384
This theorem is referenced by:  pm4.39  933  ifpbi123d  1047  3orbi123d  1438  cadbi123d  1589  eueq3  3414  sbcor  3512  unjust  3611  elun  3786  elprg  4229  eltpg  4259  rabsnifsb  4289  rabrsn  4291  preq12bg  4417  disji2  4668  disjprg  4680  disjxun  4683  swopolem  5073  sotrieq  5091  isso2i  5096  somin1  5564  ordequn  5866  fununi  6002  unpreima  6381  ordsucun  7067  funcnvuni  7161  fun11iun  7168  frxp  7332  xporderlem  7333  poxp  7334  fnwelem  7337  fnse  7339  oacan  7673  omword  7695  oeword  7715  oeoa  7722  qsdisj  7867  wemapso2lem  8498  brwdom  8513  cantnflem1  8624  r0weon  8873  infxpen  8875  sornom  9137  fin1ai  9153  isfin5  9159  isfin6  9160  sdom2en01  9162  enfin2i  9181  enfin1ai  9244  isfin5-2  9251  fin1a2lem7  9266  fin1a2lem11  9270  fin1a2lem13  9272  axdc3lem2  9311  engch  9488  eltskg  9610  tsken  9614  ltsonq  9829  addcanpr  9906  ltsosr  9953  axpre-lttri  10024  lemul1  10913  mulge0b  10931  mulle0b  10932  mulsuble0b  10933  nn1m1nn  11078  avgle  11312  nn0sub  11381  elznn0  11430  elz2  11432  nneo  11499  uztric  11747  mul2lt0bi  11974  ltxr  11987  xrrebnd  12037  xmulval  12094  xmulneg1  12137  ixxun  12229  iccsplit  12343  fzsplit2  12404  uzsplit  12450  nelfzo  12514  fzospliti  12539  fzouzsplit  12542  sqeqor  13018  swrdnd  13478  sumeq1  14463  sumeq2w  14466  sumeq2ii  14467  fz1f1o  14485  summo  14492  fsum  14495  prodeq1f  14682  prodeq2w  14686  prodeq2ii  14687  prodmo  14710  fprod  14715  ruclem12  15014  odd2np1lem  15111  dvdsprime  15447  coprm  15470  vdwapun  15725  vdwlem6  15737  vdwlem10  15741  mreexexlemd  16351  mreexexd  16355  mreexexdOLD  16356  istos  17082  tosso  17083  tsrlin  17266  tsrss  17270  isdomn  19342  prmirredlem  19889  domnchr  19928  zntoslem  19953  znfld  19957  fctop  20856  cctop  20858  ppttop  20859  pptbas  20860  isufil  21754  ufilss  21756  fixufil  21773  fin1aufil  21783  xpsdsval  22233  nlmmul0or  22534  pmltpclem1  23263  iundisj2  23363  mbfmax  23461  dvne0  23819  fta1glem2  23971  plymul0or  24081  ofmulrt  24082  quotval  24092  plydivlem3  24095  plydivlem4  24096  plydivex  24097  plydivalg  24099  quotlem  24100  aalioulem2  24133  quad2  24611  dcubic2  24616  dcubic  24618  dquartlem1  24623  dquart  24625  quart  24633  leibpilem2  24713  wilthlem1  24839  muval2  24905  perfectlem2  25000  lgslem1  25067  pntpbnd1  25320  legtrid  25531  legso  25539  ishlg  25542  lnhl  25555  symquadlem  25629  islmib  25724  isinag  25774  inaghl  25776  brbtwn2  25830  axcontlem2  25890  axcontlem4  25892  axcontlem11  25899  edglnl  26083  nb3grprlem2  26327  hashecclwwlkn1  27041  nfrgr2v  27252  h1datom  28569  atss  29333  atom1d  29340  atord  29375  chirred  29382  elimifd  29488  disji2f  29516  disjif2  29520  disjxpin  29527  iundisj2f  29529  disjunsn  29533  fzsplit3  29681  iundisj2fi  29684  f1ocnt  29687  resstos  29788  tleile  29789  trleile  29794  smatrcl  29990  fsumcvg4  30124  erdsze2lem2  31312  eqfunresadj  31785  funpsstri  31789  soseq  31879  seglelin  32348  lineunray  32379  topdifinffinlem  33325  topdifinffin  33326  topdifinfeq  33328  mblfinlem2  33577  itg2addnclem2  33592  iblabsnclem  33603  ftc1anclem5  33619  fdc1  33672  unichnidl  33960  ispridl  33963  maxidlmax  33972  lcvexchlem4  34642  lcvexchlem5  34643  2at0mat0  35129  pmapjoin  35456  cdlemg17h  36273  dihlspsnat  36939  lzunuz  37648  dvdsrabdioph  37691  acongeq12d  37863  jm2.25  37883  rmydioph  37898  expdioph  37907  fnwe2val  37936  aomclem8  37948  brfvrcld2  38301  uneqsn  38638  ntrneixb  38710  ntrneix3  38712  ntrneix13  38714  sbcorgOLD  39057  unima  39660  disjinfi  39694  salexct  40870  salexct2  40875  salexct3  40878  salgencntex  40879  salgensscntex  40880  nnfoctbdjlem  40990  nnfoctbdj  40991  iundjiun  40995  el1fzopredsuc  41660  iccpartgel  41690  divgcdoddALTV  41918  perfectALTVlem2  41956  lindslinindsimp2lem5  42576  ldepspr  42587
  Copyright terms: Public domain W3C validator