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

Theorem orbi12d 933
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 931 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 930 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 270 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wo 865
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 198  df-or 866
This theorem is referenced by:  pm4.39  990  ifpbi123d  1093  3orbi123d  1552  cadbi123d  1704  eueq3  3586  sbcor  3684  unjust  3780  elun  3959  elprg  4398  eltpg  4426  rabsnifsb  4455  rabrsn  4457  preq12bg  4580  disji2  4835  disjprg  4847  disjxun  4849  swopolem  5248  sotrieq  5266  isso2i  5271  somin1  5747  ordequn  6044  fununi  6178  unpreima  6566  ordsucun  7258  funcnvuni  7352  fun11iun  7359  frxp  7524  xporderlem  7525  poxp  7526  fnwelem  7529  fnse  7531  oacan  7868  omword  7890  oeword  7910  oeoa  7917  qsdisj  8062  wemapso2lem  8699  brwdom  8714  cantnflem1  8836  r0weon  9121  infxpen  9123  sornom  9387  fin1ai  9403  isfin5  9409  isfin6  9410  sdom2en01  9412  enfin2i  9431  enfin1ai  9494  isfin5-2  9501  fin1a2lem7  9516  fin1a2lem11  9520  fin1a2lem13  9522  axdc3lem2  9561  engch  9738  eltskg  9860  tsken  9864  ltsonq  10079  addcanpr  10156  ltsosr  10203  axpre-lttri  10274  lemul1  11163  mulge0b  11181  mulle0b  11182  mulsuble0b  11183  nn1m1nn  11328  avgle  11544  nn0sub  11612  elznn0  11661  elz2  11663  nneo  11730  uztric  11929  mul2lt0bi  12153  ltxr  12168  xrrebnd  12220  xmulval  12277  xmulneg1  12320  ixxun  12412  iccsplit  12531  fzsplit2  12592  uzsplit  12638  nelfzo  12702  fzospliti  12727  fzouzsplit  12730  sqeqor  13204  swrdnd  13659  sumeq1  14645  sumeq2w  14648  sumeq2ii  14649  fz1f1o  14667  summo  14674  fsum  14677  prodeq1f  14862  prodeq2w  14866  prodeq2ii  14867  prodmo  14890  fprod  14895  ruclem12  15193  odd2np1lem  15287  dvdsprime  15621  coprm  15643  vdwapun  15898  vdwlem6  15910  vdwlem10  15914  mreexexlemd  16512  mreexexd  16516  istos  17243  tosso  17244  tsrlin  17427  tsrss  17431  isdomn  19506  prmirredlem  20052  domnchr  20091  zntoslem  20115  znfld  20119  fctop  21026  cctop  21028  ppttop  21029  pptbas  21030  isufil  21924  ufilss  21926  fixufil  21943  fin1aufil  21953  xpsdsval  22403  nlmmul0or  22704  pmltpclem1  23435  iundisj2  23536  mbfmax  23636  dvne0  23994  fta1glem2  24146  plymul0or  24256  ofmulrt  24257  quotval  24267  plydivlem3  24270  plydivlem4  24271  plydivex  24272  plydivalg  24274  quotlem  24275  aalioulem2  24308  quad2  24786  dcubic2  24791  dcubic  24793  dquartlem1  24798  dquart  24800  quart  24808  leibpilem2  24888  wilthlem1  25014  muval2  25080  perfectlem2  25175  lgslem1  25242  pntpbnd1  25495  legtrid  25706  legso  25714  ishlg  25717  lnhl  25730  symquadlem  25804  islmib  25899  isinag  25949  inaghl  25951  brbtwn2  26005  axcontlem2  26065  axcontlem4  26067  axcontlem11  26074  edglnl  26259  nb3grprlem2  26505  hashecclwwlkn1  27234  nfrgr2v  27453  h1datom  28775  atss  29539  atom1d  29546  atord  29581  chirred  29588  elimifd  29693  disji2f  29721  disjif2  29725  disjxpin  29732  iundisj2f  29734  disjunsn  29738  fzsplit3  29886  iundisj2fi  29889  f1ocnt  29892  resstos  29991  tleile  29992  trleile  29997  smatrcl  30193  fsumcvg4  30327  erdsze2lem2  31514  eqfunresadj  31986  funpsstri  31990  soseq  32080  seglelin  32549  lineunray  32580  topdifinffinlem  33513  topdifinffin  33514  topdifinfeq  33516  mblfinlem2  33762  itg2addnclem2  33776  iblabsnclem  33787  ftc1anclem5  33803  fdc1  33855  unichnidl  34143  ispridl  34146  maxidlmax  34155  lcvexchlem4  34819  lcvexchlem5  34820  2at0mat0  35307  pmapjoin  35634  cdlemg17h  36450  dihlspsnat  37115  lzunuz  37834  dvdsrabdioph  37877  acongeq12d  38048  jm2.25  38068  rmydioph  38083  expdioph  38092  fnwe2val  38121  aomclem8  38133  brfvrcld2  38485  uneqsn  38822  ntrneixb  38894  ntrneix3  38896  ntrneix13  38898  sbcorgOLD  39239  unima  39836  disjinfi  39870  salexct  41032  salexct2  41037  salexct3  41040  salgencntex  41041  salgensscntex  41042  nnfoctbdjlem  41152  nnfoctbdj  41153  iundjiun  41157  el1fzopredsuc  41911  iccpartgel  41941  divgcdoddALTV  42169  perfectALTVlem2  42207  lindslinindsimp2lem5  42820  ldepspr  42831
  Copyright terms: Public domain W3C validator