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

Theorem orbi12i 521
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 519 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 520 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 249 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368
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 370
This theorem is referenced by:  pm4.78  582  andir  863  anddi  865  dfbi3  888  4exmid  930  cases  962  3orbi123i  1177  3or6  1300  cadcoma  1437  neorian  2720  sspsstri  3479  rexun  3557  indi  3617  symdif2  3637  unab  3638  inundif  3778  dfpr2  3913  ssunsn  4054  ssunpr  4056  sspr  4057  sstp  4058  prneimg  4074  prnebg  4075  pwpr  4108  pwtp  4109  unipr  4125  uniun  4131  iunun  4272  iunxun  4273  brun  4361  zfpair  4550  pwunss  4647  ordtri2or3  4837  opthprc  4907  xpeq0  5279  difxp  5283  ftpg  5913  ordunpr  6458  tpostpos  6786  oarec  7022  brdom2  7360  modom  7534  dfsup2  7713  wemapsolem  7785  leweon  8199  kmlem16  8355  fin23lem40  8541  axpre-lttri  9353  nn0n0n1ge2b  10665  elnn0z  10680  fz0  11486  sqeqori  11999  hashtpg  12207  cbvsum  13193  rpnnen2  13529  pythagtriplem2  13905  pythagtrip  13922  mreexexd  14607  ppttop  18633  fixufil  19517  alexsubALTlem2  19642  alexsubALTlem3  19643  alexsubALTlem4  19644  dyaddisj  21098  elim2if  25928  ofpreima2  26007  odutos  26146  trleile  26149  ordtconlem1  26376  quad3  27325  nepss  27396  cbvprod  27450  dfso2  27586  dfon2lem4  27621  dfon2lem5  27622  nofulllem5  27869  elsymdif  27876  dfon3  27945  brcup  27992  dfrdg4  28003  hfun  28238  ispridl2  28864  smprngopr  28878  isdmn3  28900  sbcori  28940  jm2.23  29371  aovov0bi  30128  bj-dfifc2  32197  bj-eltag  32566  bj-projun  32583  4atlem3  33336  elpadd  33539  paddasslem17  33576  cdlemg31b0N  34434  cdlemg31b0a  34435  cdlemh  34557
  Copyright terms: Public domain W3C validator