MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orbi12d 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  1389  eueq3  3073  sbcor  3169  sbcorg  3170  unjust  3288  elun  3452  elprg  3795  eltpg  3815  rabrsn  3838  preq12bg  3941  disji2  4163  disjprg  4172  disjxun  4174  swopolem  4476  sotrieq  4494  isso2i  4499  ordsucun  4768  somin1  5233  fununi  5480  funcnvuni  5481  fun11iun  5658  unpreima  5819  frxp  6419  xporderlem  6420  poxp  6421  fnwelem  6424  fnse  6426  oacan  6754  omword  6776  oeword  6796  oeoa  6803  qsdisj  6944  wemapso2  7481  brwdom  7495  cantnflem1  7605  r0weon  7854  infxpen  7856  sornom  8117  fin1ai  8133  isfin5  8139  isfin6  8140  sdom2en01  8142  enfin2i  8161  enfin1ai  8224  isfin5-2  8231  fin1a2lem7  8246  fin1a2lem11  8250  fin1a2lem13  8252  axdc3lem2  8291  engch  8463  eltskg  8585  tsken  8589  ltsonq  8806  addcanpr  8883  ltsosr  8929  axpre-lttri  9000  lemul1  9822  nn1m1nn  9980  avgle  10169  nn0sub  10230  elznn0  10256  elz2  10258  nneo  10313  uztric  10467  ltxr  10675  xrrebnd  10716  xmulval  10771  xmulneg1  10808  ixxun  10892  iccsplit  10989  fzsplit2  11036  uzsplit  11077  fzospliti  11124  fzouzsplit  11127  sqeqor  11454  sumeq1f  12441  sumeq2w  12445  sumeq2ii  12446  cbvsum  12448  fz1f1o  12463  summo  12470  fsum  12473  ruclem12  12799  odd2np1lem  12866  dvdsprime  13051  coprm  13059  vdwapun  13301  vdwlem6  13313  vdwlem10  13317  mreexexlemd  13828  mreexexd  13832  istos  14423  tosso  14424  tsrlin  14610  tsrss  14614  isdomn  16313  prmirredlem  16732  domnchr  16772  zntoslem  16796  znfld  16800  fctop  17027  cctop  17029  ppttop  17030  pptbas  17031  isufil  17892  ufilss  17894  fixufil  17911  fin1aufil  17921  xpsdsval  18368  nlmmul0or  18676  pmltpclem1  19302  iundisj2  19400  mbfmax  19498  dvne0  19852  fta1glem2  20046  plymul0or  20155  ofmulrt  20156  quotval  20166  plydivlem3  20169  plydivlem4  20170  plydivex  20171  plydivalg  20173  quotlem  20174  aalioulem2  20207  quad2  20636  dcubic2  20641  dcubic  20643  dquartlem1  20648  dquart  20650  quart  20658  leibpilem2  20738  wilthlem1  20808  muval2  20874  perfectlem2  20971  lgslem1  21037  pntpbnd1  21237  nb3graprlem2  21418  h1datom  23041  atss  23806  atom1d  23813  atord  23848  chirred  23855  elimifd  23961  disji2f  23976  disjif2  23980  disjxpin  23985  iundisj2f  23987  fzsplit3  24107  iundisj2fi  24110  resstos  24145  tleile  24146  erdsze2lem2  24847  mulge0b  25148  mulle0b  25149  mulsuble0b  25150  prodeq1f  25191  prodeq2w  25195  prodeq2ii  25196  prodmo  25219  fprod  25224  funpsstri  25339  soseq  25472  brbtwn2  25752  axcontlem2  25812  axcontlem4  25814  axcontlem11  25821  seglelin  25958  lineunray  25989  mblfinlem  26147  itg2addnclem2  26160  iblabsnclem  26171  fdc1  26344  unichnidl  26535  ispridl  26538  maxidlmax  26547  lzunuz  26720  dvdsrabdioph  26764  acongeq12d  26938  jm2.25  26964  rmydioph  26979  expdioph  26988  fnwe2val  27018  aomclem8  27031  frgra2v  28107  lcvexchlem4  29524  lcvexchlem5  29525  2at0mat0  30011  pmapjoin  30338  cdlemg17h  31154  dihlspsnat  31820
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