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

Theorem orbi12d 691
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 684 . 2  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
3 bi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43orbi2d 683 . 2  |-  ( ph  ->  ( ( ch  \/  th )  <->  ( ch  \/  ta ) ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358
This theorem is referenced by:  pm4.39  842  3orbi123d  1253  cadbi123d  1392  eueq3  3101  sbcor  3197  sbcorg  3198  unjust  3316  elun  3480  elprg  3823  eltpg  3843  rabrsn  3866  preq12bg  3969  disji2  4191  disjprg  4200  disjxun  4202  swopolem  4504  sotrieq  4522  isso2i  4527  ordsucun  4797  somin1  5262  fununi  5509  funcnvuni  5510  fun11iun  5687  unpreima  5848  frxp  6448  xporderlem  6449  poxp  6450  fnwelem  6453  fnse  6455  oacan  6783  omword  6805  oeword  6825  oeoa  6832  qsdisj  6973  wemapso2  7513  brwdom  7527  cantnflem1  7637  r0weon  7886  infxpen  7888  sornom  8149  fin1ai  8165  isfin5  8171  isfin6  8172  sdom2en01  8174  enfin2i  8193  enfin1ai  8256  isfin5-2  8263  fin1a2lem7  8278  fin1a2lem11  8282  fin1a2lem13  8284  axdc3lem2  8323  engch  8495  eltskg  8617  tsken  8621  ltsonq  8838  addcanpr  8915  ltsosr  8961  axpre-lttri  9032  lemul1  9854  nn1m1nn  10012  avgle  10201  nn0sub  10262  elznn0  10288  elz2  10290  nneo  10345  uztric  10499  ltxr  10707  xrrebnd  10748  xmulval  10803  xmulneg1  10840  ixxun  10924  iccsplit  11021  fzsplit2  11068  uzsplit  11110  fzospliti  11157  fzouzsplit  11160  sqeqor  11487  sumeq1f  12474  sumeq2w  12478  sumeq2ii  12479  cbvsum  12481  fz1f1o  12496  summo  12503  fsum  12506  ruclem12  12832  odd2np1lem  12899  dvdsprime  13084  coprm  13092  vdwapun  13334  vdwlem6  13346  vdwlem10  13350  mreexexlemd  13861  mreexexd  13865  istos  14456  tosso  14457  tsrlin  14643  tsrss  14647  isdomn  16346  prmirredlem  16765  domnchr  16805  zntoslem  16829  znfld  16833  fctop  17060  cctop  17062  ppttop  17063  pptbas  17064  isufil  17927  ufilss  17929  fixufil  17946  fin1aufil  17956  xpsdsval  18403  nlmmul0or  18711  pmltpclem1  19337  iundisj2  19435  mbfmax  19533  dvne0  19887  fta1glem2  20081  plymul0or  20190  ofmulrt  20191  quotval  20201  plydivlem3  20204  plydivlem4  20205  plydivex  20206  plydivalg  20208  quotlem  20209  aalioulem2  20242  quad2  20671  dcubic2  20676  dcubic  20678  dquartlem1  20683  dquart  20685  quart  20693  leibpilem2  20773  wilthlem1  20843  muval2  20909  perfectlem2  21006  lgslem1  21072  pntpbnd1  21272  nb3graprlem2  21453  h1datom  23076  atss  23841  atom1d  23848  atord  23883  chirred  23890  elimifd  23996  disji2f  24011  disjif2  24015  disjxpin  24020  iundisj2f  24022  fzsplit3  24142  iundisj2fi  24145  resstos  24180  tleile  24181  erdsze2lem2  24882  mulge0b  25183  mulle0b  25184  mulsuble0b  25185  prodeq1f  25226  prodeq2w  25230  prodeq2ii  25231  prodmo  25254  fprod  25259  funpsstri  25381  soseq  25521  brbtwn2  25836  axcontlem2  25896  axcontlem4  25898  axcontlem11  25905  seglelin  26042  lineunray  26073  mblfinlem  26234  itg2addnclem2  26247  iblabsnclem  26258  ftc1anclem5  26274  fdc1  26441  unichnidl  26632  ispridl  26635  maxidlmax  26644  lzunuz  26817  dvdsrabdioph  26861  acongeq12d  27035  jm2.25  27061  rmydioph  27076  expdioph  27085  fnwe2val  27115  aomclem8  27127  frgra2v  28326  lcvexchlem4  29772  lcvexchlem5  29773  2at0mat0  30259  pmapjoin  30586  cdlemg17h  31402  dihlspsnat  32068
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 178  df-or 360
  Copyright terms: Public domain W3C validator