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

Theorem orbi12i 523
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 521 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 522 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 252 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    \/ wo 369
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 188  df-or 371
This theorem is referenced by:  pm4.78  584  andir  876  anddi  878  dfbi3  901  4exmid  947  cases  979  3orbi123i  1195  3or6  1346  cadcoma  1510  neorian  2758  sspsstri  3573  rexun  3652  elsymdif  3704  symdif2  3707  indi  3725  unab  3746  inundif  3879  dfpr2  4017  ssunsn  4163  ssunpr  4165  sspr  4166  sstp  4167  prneimg  4184  prnebg  4185  pwpr  4218  pwtp  4219  unipr  4235  uniun  4241  iunun  4386  iunxun  4387  brun  4474  zfpair  4659  pwunss  4759  opthprc  4902  xpeq0  5277  difxp  5281  ordtri2or3  5539  ftpg  6089  ordunpr  6667  tpostpos  7001  oarec  7271  brdom2  7606  modom  7779  dfsup2  7964  wemapsolem  8065  leweon  8441  kmlem16  8593  fin23lem40  8779  axpre-lttri  9588  nn0n0n1ge2b  10933  elnn0z  10950  fz0  11812  sqeqori  12383  hashtpg  12632  cbvsum  13739  cbvprod  13947  rpnnen2  14256  lcmfpr  14571  pythagtriplem2  14730  pythagtrip  14747  mreexexd  15505  ppttop  19953  fixufil  20868  alexsubALTlem2  20994  alexsubALTlem3  20995  alexsubALTlem4  20996  dyaddisj  22431  ofpreima2  28109  odutos  28262  trleile  28265  smatrcl  28461  ordtconlem1  28569  sitgaddlemb  29009  quad3  30090  nepss  30138  dfso2  30181  dfon2lem4  30219  dfon2lem5  30220  nofulllem5  30380  dfon3  30444  brcup  30491  dfrdg4  30503  hfun  30730  bj-dfifc2  30943  bj-eltag  31320  bj-projun  31337  poimirlem22  31669  poimirlem31  31678  poimirlem32  31679  ispridl2  31978  smprngopr  31992  isdmn3  32014  sbcori  32053  tsbi4  32085  4atlem3  32873  elpadd  33076  paddasslem17  33113  cdlemg31b0N  33973  cdlemg31b0a  33974  cdlemh  34096  jm2.23  35560  ifpim123g  35846  ifpananb  35852  rp-isfinite6  35865  iunrelexp0  35936  aovov0bi  38100  zeoALTV  38201  divgcdoddALTV  38213
  Copyright terms: Public domain W3C validator