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  1373  eueq3  2940  sbcor  3035  sbcorg  3036  unjust  3156  elun  3316  elprg  3657  eltpg  3676  preq12bg  3791  disji2  4010  disjprg  4019  disjxun  4021  swopolem  4323  sotrieq  4341  isso2i  4346  ordsucun  4616  somin1  5079  fununi  5316  funcnvuni  5317  fun11iun  5493  unpreima  5651  frxp  6225  xporderlem  6226  poxp  6227  fnwelem  6230  fnse  6232  oacan  6546  omword  6568  oeword  6588  oeoa  6595  qsdisj  6736  wemapso2  7267  brwdom  7281  cantnflem1  7391  r0weon  7640  infxpen  7642  sornom  7903  fin1ai  7919  isfin5  7925  isfin6  7926  sdom2en01  7928  enfin2i  7947  enfin1ai  8010  isfin5-2  8017  fin1a2lem7  8032  fin1a2lem11  8036  fin1a2lem13  8038  axdc3lem2  8077  engch  8250  eltskg  8372  tsken  8376  ltsonq  8593  addcanpr  8670  ltsosr  8716  axpre-lttri  8787  lemul1  9608  nn1m1nn  9766  avgle  9953  nn0sub  10014  elznn0  10038  elz2  10040  nneo  10095  uztric  10249  ltxr  10457  xrrebnd  10497  xmulval  10552  xmulneg1  10589  ixxun  10672  iccsplit  10768  fzsplit2  10815  uzsplit  10855  fzospliti  10898  fzouzsplit  10901  sqeqor  11217  sumeq1f  12161  sumeq2w  12165  sumeq2ii  12166  cbvsum  12168  fz1f1o  12183  summo  12190  fsum  12193  ruclem12  12519  odd2np1lem  12586  dvdsprime  12771  coprm  12779  vdwapun  13021  vdwlem6  13033  vdwlem10  13037  mreexexlemd  13546  mreexexd  13550  istos  14141  tosso  14142  tsrlin  14328  tsrss  14332  isdomn  16035  prmirredlem  16446  domnchr  16486  zntoslem  16510  znfld  16514  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  isufil  17598  ufilss  17600  fixufil  17617  fin1aufil  17627  xpsdsval  17945  nlmmul0or  18194  pmltpclem1  18808  iundisj2  18906  mbfmax  19004  dvne0  19358  fta1glem2  19552  plymul0or  19661  ofmulrt  19662  quotval  19672  plydivlem3  19675  plydivlem4  19676  plydivex  19677  plydivalg  19679  quotlem  19680  aalioulem2  19713  quad2  20135  dcubic2  20140  dcubic  20142  dquartlem1  20147  dquart  20149  quart  20157  leibpilem2  20237  wilthlem1  20306  muval2  20372  perfectlem2  20469  lgslem1  20535  pntpbnd1  20735  h1datom  22161  atss  22926  atom1d  22933  atord  22968  chirred  22975  fzsplit3  23031  elimifd  23151  disji2f  23354  disjif2  23358  iundisj2fi  23364  iundisj2f  23366  erdsze2lem2  23735  mulge0b  24086  mulle0b  24087  mulsuble0b  24088  funpsstri  24121  soseq  24254  brbtwn2  24533  axcontlem2  24593  axcontlem4  24595  axcontlem11  24602  seglelin  24739  lineunray  24770  srefwref  25067  nelioo5  25511  vtarsuelt  25895  partarelt1  25896  partarelt2  25897  bhp2a  26176  fdc1  26456  unichnidl  26656  ispridl  26659  maxidlmax  26668  lzunuz  26847  dvdsrabdioph  26891  acongeq12d  27066  jm2.25  27092  rmydioph  27107  expdioph  27116  fnwe2val  27146  aomclem8  27159  frgra2v  28177  lcvexchlem4  29227  lcvexchlem5  29228  2at0mat0  29714  pmapjoin  30041  cdlemg17h  30857  dihlspsnat  31523
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