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

Theorem orbi12i 507
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 505 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 506 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 240 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357
This theorem is referenced by:  pm4.78  565  andir  838  anddi  840  dfbi3  863  4exmid  905  3orbi123i  1141  3or6  1263  cadcoma  1386  neorian  2566  sspsstri  3312  rexun  3389  indi  3449  symdif2  3468  unab  3469  inundif  3566  elimif  3628  dfpr2  3690  ssunsn  3811  ssunpr  3813  sspr  3814  sstp  3815  pwpr  3860  pwtp  3861  unipr  3878  uniun  3883  iunun  4019  iunxun  4020  brun  4106  zfpair  4249  pwunss  4335  pwundifOLD  4338  ordtri2or3  4527  ordunpr  4654  opthprc  4773  xpeq0  5137  difxp  6195  tpostpos  6296  oarec  6602  brdom2  6934  modom  7106  dfsup2  7240  wemapso2lem  7310  leweon  7684  kmlem16  7836  fin23lem40  8022  axpre-lttri  8832  elnn0z  10083  sqeqori  11262  rpnnen2  12551  pythagtriplem2  12917  pythagtrip  12934  mreexexd  13599  ppttop  16800  fixufil  17669  alexsubALTlem2  17794  alexsubALTlem3  17795  alexsubALTlem4  17796  dyaddisj  19004  elim2if  23148  nepss  24356  cbvprod  24418  dfso2  24496  dfon2lem4  24527  dfon2lem5  24528  nofulllem5  24745  elsymdif  24752  dfon3  24817  brcup  24863  dfrdg4  24874  hfun  25194  ispridl2  25811  smprngopr  25825  isdmn3  25847  jm2.23  26237  aovov0bi  27209  prneimg  27228  ftpg  27234  hashtpg  27279  ax12conj2  28926  a12study8  28937  a12peros  28939  4atlem3  29603  elpadd  29806  paddasslem17  29843  cdlemg31b0N  30701  cdlemg31b0a  30702  cdlemh  30824
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 177  df-or 359
  Copyright terms: Public domain W3C validator