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

Theorem orbi12i 530
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 528 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 529 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 257 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    \/ wo 375
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 190  df-or 377
This theorem is referenced by:  pm4.78  592  andir  885  anddi  887  dfbi3  910  4exmid  954  cases  981  3orbi123i  1220  3or6  1376  cadcoma  1523  neorian  2737  sspsstri  3521  rexun  3605  elsymdif  3659  symdif2  3662  indi  3680  unab  3701  dfnf5  3752  inundif  3836  dfpr2  3974  ssunsn  4124  ssunpr  4126  sspr  4127  sstp  4128  prneimg  4148  prnebg  4149  pwpr  4186  pwtp  4187  unipr  4203  uniun  4209  iunun  4353  iunxun  4354  brun  4444  zfpair  4637  pwunss  4744  opthprc  4887  xpeq0  5263  difxp  5267  ordtri2or3  5527  ftpg  6090  ordunpr  6672  mpt2xneldm  6977  tpostpos  7011  oarec  7281  brdom2  7617  modom  7791  dfsup2  7976  wemapsolem  8083  leweon  8460  kmlem16  8613  fin23lem40  8799  axpre-lttri  9607  nn0n0n1ge2b  10957  elnn0z  10974  fz0  11840  sqeqori  12424  hashtpg  12682  cbvsum  13838  cbvprod  14046  rpnnen2  14355  lcmfpr  14679  pythagtriplem2  14846  pythagtrip  14863  mreexexd  15632  ppttop  20099  fixufil  21015  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALTlem4  21143  dyaddisj  22633  ofpreima2  28344  odutos  28499  trleile  28502  smatrcl  28696  ordtconlem1  28804  sitgaddlemb  29254  quad3  30374  nepss  30422  dfso2  30465  dfon2lem4  30503  dfon2lem5  30504  nofulllem5  30666  dfon3  30730  brcup  30777  dfrdg4  30789  hfun  31016  bj-dfifc2  31222  bj-eltag  31641  bj-projun  31658  poimirlem22  32026  poimirlem31  32035  poimirlem32  32036  ispridl2  32335  smprngopr  32349  isdmn3  32371  sbcori  32410  tsbi4  32442  4atlem3  33232  elpadd  33435  paddasslem17  33472  cdlemg31b0N  34332  cdlemg31b0a  34333  cdlemh  34455  jm2.23  35922  ifpim123g  36215  ifpananb  36221  rp-isfinite6  36234  iunrelexp0  36365  aovov0bi  38843  zeoALTV  38944  divgcdoddALTV  38956  propeqop  39146
  Copyright terms: Public domain W3C validator