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

Theorem orbi12d 748
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 741 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 bi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43orbi2d 740 . 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  951  ifpbi123d  1065  3orbi123d  1535  cadbi123d  1686  eueq3  3510  sbcor  3608  unjust  3707  elun  3884  elprg  4329  eltpg  4359  rabsnifsb  4389  rabrsn  4391  preq12bg  4518  disji2  4776  disjprg  4788  disjxun  4790  swopolem  5184  sotrieq  5202  isso2i  5207  somin1  5675  ordequn  5977  fununi  6113  unpreima  6492  ordsucun  7178  funcnvuni  7272  fun11iun  7279  frxp  7443  xporderlem  7444  poxp  7445  fnwelem  7448  fnse  7450  oacan  7785  omword  7807  oeword  7827  oeoa  7834  qsdisj  7979  wemapso2lem  8610  brwdom  8625  cantnflem1  8747  r0weon  8996  infxpen  8998  sornom  9262  fin1ai  9278  isfin5  9284  isfin6  9285  sdom2en01  9287  enfin2i  9306  enfin1ai  9369  isfin5-2  9376  fin1a2lem7  9391  fin1a2lem11  9395  fin1a2lem13  9397  axdc3lem2  9436  engch  9613  eltskg  9735  tsken  9739  ltsonq  9954  addcanpr  10031  ltsosr  10078  axpre-lttri  10149  lemul1  11038  mulge0b  11056  mulle0b  11057  mulsuble0b  11058  nn1m1nn  11203  avgle  11437  nn0sub  11506  elznn0  11555  elz2  11557  nneo  11624  uztric  11872  mul2lt0bi  12100  ltxr  12113  xrrebnd  12163  xmulval  12220  xmulneg1  12263  ixxun  12355  iccsplit  12469  fzsplit2  12530  uzsplit  12576  nelfzo  12640  fzospliti  12665  fzouzsplit  12668  sqeqor  13143  swrdnd  13603  sumeq1  14589  sumeq2w  14592  sumeq2ii  14593  fz1f1o  14611  summo  14618  fsum  14621  prodeq1f  14808  prodeq2w  14812  prodeq2ii  14813  prodmo  14836  fprod  14841  ruclem12  15140  odd2np1lem  15237  dvdsprime  15573  coprm  15596  vdwapun  15851  vdwlem6  15863  vdwlem10  15867  mreexexlemd  16477  mreexexd  16481  istos  17207  tosso  17208  tsrlin  17391  tsrss  17395  isdomn  19467  prmirredlem  20014  domnchr  20053  zntoslem  20078  znfld  20082  fctop  20981  cctop  20983  ppttop  20984  pptbas  20985  isufil  21879  ufilss  21881  fixufil  21898  fin1aufil  21908  xpsdsval  22358  nlmmul0or  22659  pmltpclem1  23388  iundisj2  23488  mbfmax  23586  dvne0  23944  fta1glem2  24096  plymul0or  24206  ofmulrt  24207  quotval  24217  plydivlem3  24220  plydivlem4  24221  plydivex  24222  plydivalg  24224  quotlem  24225  aalioulem2  24258  quad2  24736  dcubic2  24741  dcubic  24743  dquartlem1  24748  dquart  24750  quart  24758  leibpilem2  24838  wilthlem1  24964  muval2  25030  perfectlem2  25125  lgslem1  25192  pntpbnd1  25445  legtrid  25656  legso  25664  ishlg  25667  lnhl  25680  symquadlem  25754  islmib  25849  isinag  25899  inaghl  25901  brbtwn2  25955  axcontlem2  26015  axcontlem4  26017  axcontlem11  26024  edglnl  26208  nb3grprlem2  26452  hashecclwwlkn1  27179  nfrgr2v  27397  h1datom  28721  atss  29485  atom1d  29492  atord  29527  chirred  29534  elimifd  29640  disji2f  29668  disjif2  29672  disjxpin  29679  iundisj2f  29681  disjunsn  29685  fzsplit3  29833  iundisj2fi  29836  f1ocnt  29839  resstos  29940  tleile  29941  trleile  29946  smatrcl  30142  fsumcvg4  30276  erdsze2lem2  31464  eqfunresadj  31937  funpsstri  31941  soseq  32031  seglelin  32500  lineunray  32531  topdifinffinlem  33477  topdifinffin  33478  topdifinfeq  33480  mblfinlem2  33729  itg2addnclem2  33744  iblabsnclem  33755  ftc1anclem5  33771  fdc1  33824  unichnidl  34112  ispridl  34115  maxidlmax  34124  lcvexchlem4  34796  lcvexchlem5  34797  2at0mat0  35283  pmapjoin  35610  cdlemg17h  36427  dihlspsnat  37093  lzunuz  37802  dvdsrabdioph  37845  acongeq12d  38017  jm2.25  38037  rmydioph  38052  expdioph  38061  fnwe2val  38090  aomclem8  38102  brfvrcld2  38455  uneqsn  38792  ntrneixb  38864  ntrneix3  38866  ntrneix13  38868  sbcorgOLD  39211  unima  39814  disjinfi  39848  salexct  41024  salexct2  41029  salexct3  41032  salgencntex  41033  salgensscntex  41034  nnfoctbdjlem  41144  nnfoctbdj  41145  iundjiun  41149  el1fzopredsuc  41814  iccpartgel  41844  divgcdoddALTV  42072  perfectALTVlem2  42110  lindslinindsimp2lem5  42730  ldepspr  42741
  Copyright terms: Public domain W3C validator