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

Theorem orbi12i 519
Description: Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-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 517 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 518 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 249 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 366
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 185  df-or 368
This theorem is referenced by:  pm4.78  580  andir  866  anddi  868  dfbi3  891  4exmid  937  cases  968  3orbi123i  1184  3or6  1308  cadcoma  1465  neorian  2781  sspsstri  3592  rexun  3670  elsymdif  3720  symdif2  3723  indi  3741  unab  3762  inundif  3894  dfpr2  4031  ssunsn  4176  ssunpr  4178  sspr  4179  sstp  4180  prneimg  4197  prnebg  4198  pwpr  4231  pwtp  4232  unipr  4248  uniun  4254  iunun  4399  iunxun  4400  brun  4487  zfpair  4674  pwunss  4774  ordtri2or3  4964  opthprc  5036  xpeq0  5412  difxp  5416  ftpg  6057  ordunpr  6634  tpostpos  6967  oarec  7203  brdom2  7538  modom  7713  dfsup2  7894  wemapsolem  7967  leweon  8380  kmlem16  8536  fin23lem40  8722  axpre-lttri  9531  nn0n0n1ge2b  10856  elnn0z  10873  fz0  11704  sqeqori  12265  hashtpg  12510  cbvsum  13602  cbvprod  13807  rpnnen2  14046  pythagtriplem2  14428  pythagtrip  14445  mreexexd  15140  ppttop  19678  fixufil  20592  alexsubALTlem2  20717  alexsubALTlem3  20718  alexsubALTlem4  20719  dyaddisj  22174  ofpreima2  27738  odutos  27888  trleile  27891  ordtconlem1  28144  quad3  29291  nepss  29339  dfso2  29427  dfon2lem4  29461  dfon2lem5  29462  nofulllem5  29709  dfon3  29773  brcup  29820  dfrdg4  29831  hfun  30066  ispridl2  30678  smprngopr  30692  isdmn3  30714  sbcori  30754  tsbi4  30786  jm2.23  31180  aovov0bi  32523  zeoALTV  32584  divgcdoddALTV  32596  bj-dfifc2  34584  bj-eltag  34955  bj-projun  34972  4atlem3  35736  elpadd  35939  paddasslem17  35976  cdlemg31b0N  36836  cdlemg31b0a  36837  cdlemh  36959  ifpim123g  38122  ifpananb  38164  rp-isfinite6  38176  iunrelexp0  38245
  Copyright terms: Public domain W3C validator