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

Theorem orbi12i 508
Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
orbi12i.1  |-  ( ph  <->  ps )
orbi12i.2  |-  ( ch  <->  th )
Assertion
Ref Expression
orbi12i  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)

Proof of Theorem orbi12i
StepHypRef Expression
1 orbi12i.2 . . 3  |-  ( ch  <->  th )
21orbi2i 506 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 507 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 241 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358
This theorem is referenced by:  pm4.78  566  andir  839  anddi  841  dfbi3  864  4exmid  906  3orbi123i  1143  3or6  1265  cadcoma  1404  neorian  2685  sspsstri  3441  rexun  3519  indi  3579  symdif2  3599  unab  3600  inundif  3698  elimif  3760  dfpr2  3822  ssunsn  3951  ssunpr  3953  sspr  3954  sstp  3955  prneimg  3970  prnebg  3971  pwpr  4003  pwtp  4004  unipr  4021  uniun  4026  iunun  4163  iunxun  4164  brun  4250  zfpair  4393  pwunss  4480  ordtri2or3  4671  ordunpr  4798  opthprc  4917  xpeq0  5285  ftpg  5908  difxp  6372  tpostpos  6491  oarec  6797  brdom2  7129  modom  7301  dfsup2  7439  wemapso2lem  7511  leweon  7885  kmlem16  8037  fin23lem40  8223  axpre-lttri  9032  nn0n0n1ge2b  10273  elnn0z  10286  sqeqori  11485  hashtpg  11683  rpnnen2  12817  pythagtriplem2  13183  pythagtrip  13200  mreexexd  13865  ppttop  17063  fixufil  17946  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  dyaddisj  19480  elim2if  23997  sibfof  24646  nepss  25167  cbvprod  25233  dfso2  25369  dfon2lem4  25405  dfon2lem5  25406  nofulllem5  25653  elsymdif  25660  dfon3  25729  brcup  25776  dfrdg4  25787  hfun  26111  ispridl2  26629  smprngopr  26643  isdmn3  26665  jm2.23  27048  aovov0bi  28017  4atlem3  30320  elpadd  30523  paddasslem17  30560  cdlemg31b0N  31418  cdlemg31b0a  31419  cdlemh  31541
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