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

Theorem orbi12d 692
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 685 . 2  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  th ) ) )
3 bi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43orbi2d 684 . 2  |-  ( ph  ->  ( ( ch  \/  th )  <->  ( ch  \/  ta ) ) )
52, 4bitrd 246 1  |-  ( ph  ->  ( ( ps  \/  th )  <->  ( ch  \/  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    \/ wo 359
This theorem is referenced by:  pm4.39  843  3orbi123d  1254  cadbi123d  1393  eueq3  3111  sbcor  3207  sbcorg  3208  unjust  3326  elun  3490  elprg  3833  eltpg  3853  rabrsn  3876  preq12bg  3979  disji2  4202  disjprg  4211  disjxun  4213  swopolem  4515  sotrieq  4533  isso2i  4538  ordsucun  4808  somin1  5273  fununi  5520  funcnvuni  5521  fun11iun  5698  unpreima  5859  frxp  6459  xporderlem  6460  poxp  6461  fnwelem  6464  fnse  6466  oacan  6794  omword  6816  oeword  6836  oeoa  6843  qsdisj  6984  wemapso2  7524  brwdom  7538  cantnflem1  7648  r0weon  7899  infxpen  7901  sornom  8162  fin1ai  8178  isfin5  8184  isfin6  8185  sdom2en01  8187  enfin2i  8206  enfin1ai  8269  isfin5-2  8276  fin1a2lem7  8291  fin1a2lem11  8295  fin1a2lem13  8297  axdc3lem2  8336  engch  8508  eltskg  8630  tsken  8634  ltsonq  8851  addcanpr  8928  ltsosr  8974  axpre-lttri  9045  lemul1  9867  nn1m1nn  10025  avgle  10214  nn0sub  10275  elznn0  10301  elz2  10303  nneo  10358  uztric  10512  ltxr  10720  xrrebnd  10761  xmulval  10816  xmulneg1  10853  ixxun  10937  iccsplit  11034  fzsplit2  11081  uzsplit  11123  fzospliti  11170  fzouzsplit  11173  sqeqor  11500  sumeq1f  12487  sumeq2w  12491  sumeq2ii  12492  cbvsum  12494  fz1f1o  12509  summo  12516  fsum  12519  ruclem12  12845  odd2np1lem  12912  dvdsprime  13097  coprm  13105  vdwapun  13347  vdwlem6  13359  vdwlem10  13363  mreexexlemd  13874  mreexexd  13878  istos  14469  tosso  14470  tsrlin  14656  tsrss  14660  isdomn  16359  prmirredlem  16778  domnchr  16818  zntoslem  16842  znfld  16846  fctop  17073  cctop  17075  ppttop  17076  pptbas  17077  isufil  17940  ufilss  17942  fixufil  17959  fin1aufil  17969  xpsdsval  18416  nlmmul0or  18724  pmltpclem1  19350  iundisj2  19448  mbfmax  19544  dvne0  19900  fta1glem2  20094  plymul0or  20203  ofmulrt  20204  quotval  20214  plydivlem3  20217  plydivlem4  20218  plydivex  20219  plydivalg  20221  quotlem  20222  aalioulem2  20255  quad2  20684  dcubic2  20689  dcubic  20691  dquartlem1  20696  dquart  20698  quart  20706  leibpilem2  20786  wilthlem1  20856  muval2  20922  perfectlem2  21019  lgslem1  21085  pntpbnd1  21285  nb3graprlem2  21466  h1datom  23089  atss  23854  atom1d  23861  atord  23896  chirred  23903  elimifd  24009  disji2f  24024  disjif2  24028  disjxpin  24033  iundisj2f  24035  fzsplit3  24155  iundisj2fi  24158  resstos  24193  tleile  24194  erdsze2lem2  24895  mulge0b  25196  mulle0b  25197  mulsuble0b  25198  prodeq1f  25239  prodeq2w  25243  prodeq2ii  25244  prodmo  25267  fprod  25272  funpsstri  25394  soseq  25534  brbtwn2  25849  axcontlem2  25909  axcontlem4  25911  axcontlem11  25918  seglelin  26055  lineunray  26086  mblfinlem2  26256  itg2addnclem2  26271  iblabsnclem  26282  ftc1anclem5  26298  fdc1  26464  unichnidl  26655  ispridl  26658  maxidlmax  26667  lzunuz  26840  dvdsrabdioph  26884  acongeq12d  27058  jm2.25  27084  rmydioph  27099  expdioph  27108  fnwe2val  27138  aomclem8  27150  frgra2v  28463  lcvexchlem4  29909  lcvexchlem5  29910  2at0mat0  30396  pmapjoin  30723  cdlemg17h  31539  dihlspsnat  32205
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 179  df-or 361
  Copyright terms: Public domain W3C validator