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

Theorem orbi12d 690
Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
orbi12d  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )

Proof of Theorem orbi12d
StepHypRef Expression
1 bi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21orbi1d 683 . 2  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
3 bi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43orbi2d 682 . 2  |-  ( ph  ->  ( ( ch  \/  th )  <->  ( ch  \/  ta ) ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357
This theorem is referenced by:  pm4.39  841  3orbi123d  1251  cadbi123d  1383  eueq3  3016  sbcor  3111  sbcorg  3112  unjust  3232  elun  3392  elprg  3733  eltpg  3752  preq12bg  3872  disji2  4091  disjprg  4100  disjxun  4102  swopolem  4405  sotrieq  4423  isso2i  4428  ordsucun  4698  somin1  5161  fununi  5398  funcnvuni  5399  fun11iun  5576  unpreima  5734  frxp  6312  xporderlem  6313  poxp  6314  fnwelem  6317  fnse  6319  oacan  6633  omword  6655  oeword  6675  oeoa  6682  qsdisj  6823  wemapso2  7357  brwdom  7371  cantnflem1  7481  r0weon  7730  infxpen  7732  sornom  7993  fin1ai  8009  isfin5  8015  isfin6  8016  sdom2en01  8018  enfin2i  8037  enfin1ai  8100  isfin5-2  8107  fin1a2lem7  8122  fin1a2lem11  8126  fin1a2lem13  8128  axdc3lem2  8167  engch  8340  eltskg  8462  tsken  8466  ltsonq  8683  addcanpr  8760  ltsosr  8806  axpre-lttri  8877  lemul1  9698  nn1m1nn  9856  avgle  10045  nn0sub  10106  elznn0  10130  elz2  10132  nneo  10187  uztric  10341  ltxr  10549  xrrebnd  10589  xmulval  10644  xmulneg1  10681  ixxun  10764  iccsplit  10860  fzsplit2  10907  uzsplit  10947  fzospliti  10990  fzouzsplit  10993  sqeqor  11310  sumeq1f  12258  sumeq2w  12262  sumeq2ii  12263  cbvsum  12265  fz1f1o  12280  summo  12287  fsum  12290  ruclem12  12616  odd2np1lem  12683  dvdsprime  12868  coprm  12876  vdwapun  13118  vdwlem6  13130  vdwlem10  13134  mreexexlemd  13645  mreexexd  13649  istos  14240  tosso  14241  tsrlin  14427  tsrss  14431  isdomn  16134  prmirredlem  16552  domnchr  16592  zntoslem  16616  znfld  16620  fctop  16847  cctop  16849  ppttop  16850  pptbas  16851  isufil  17700  ufilss  17702  fixufil  17719  fin1aufil  17729  xpsdsval  18047  nlmmul0or  18296  pmltpclem1  18912  iundisj2  19010  mbfmax  19108  dvne0  19462  fta1glem2  19656  plymul0or  19765  ofmulrt  19766  quotval  19776  plydivlem3  19779  plydivlem4  19780  plydivex  19781  plydivalg  19783  quotlem  19784  aalioulem2  19817  quad2  20246  dcubic2  20251  dcubic  20253  dquartlem1  20258  dquart  20260  quart  20268  leibpilem2  20348  wilthlem1  20418  muval2  20484  perfectlem2  20581  lgslem1  20647  pntpbnd1  20847  h1datom  22275  atss  23040  atom1d  23047  atord  23082  chirred  23089  elimifd  23203  disji2f  23218  disjif2  23222  iundisj2f  23228  fzsplit3  23352  iundisj2fi  23357  erdsze2lem2  24139  mulge0b  24492  mulle0b  24493  mulsuble0b  24494  prodeq1f  24535  prodeq2w  24539  prodeq2ii  24540  prodmo  24563  fprod  24568  funpsstri  24679  soseq  24812  brbtwn2  25092  axcontlem2  25152  axcontlem4  25154  axcontlem11  25161  seglelin  25298  lineunray  25329  itg2addnclem2  25493  itgaddnclem2  25499  iblabsnclem  25503  fdc1  25780  unichnidl  25979  ispridl  25982  maxidlmax  25991  lzunuz  26170  dvdsrabdioph  26214  acongeq12d  26389  jm2.25  26415  rmydioph  26430  expdioph  26439  fnwe2val  26469  aomclem8  26482  rabrsn  27413  nb3graprlem2  27615  frgra2v  27832  lcvexchlem4  29296  lcvexchlem5  29297  2at0mat0  29783  pmapjoin  30110  cdlemg17h  30926  dihlspsnat  31592
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator