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  1385  neorian  2533  sspsstri  3278  rexun  3355  indi  3415  symdif2  3434  unab  3435  inundif  3532  elimif  3594  dfpr2  3656  ssunsn  3774  ssunpr  3776  sspr  3777  sstp  3778  pwpr  3823  pwtp  3824  unipr  3841  uniun  3846  iunun  3982  iunxun  3983  brun  4069  zfpair  4212  pwunss  4298  pwundifOLD  4301  ordtri2or3  4490  ordunpr  4617  opthprc  4736  xpeq0  5100  difxp  6153  tpostpos  6254  oarec  6560  brdom2  6891  modom  7063  dfsup2  7195  wemapso2lem  7265  leweon  7639  kmlem16  7791  fin23lem40  7977  axpre-lttri  8787  elnn0z  10036  sqeqori  11215  rpnnen2  12504  pythagtriplem2  12870  pythagtrip  12887  mreexexd  13550  ppttop  16744  fixufil  17617  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  dyaddisj  18951  elim2if  23152  nepss  24072  dfso2  24111  dfon2lem4  24142  dfon2lem5  24143  nofulllem5  24360  elsymdif  24367  dfon3  24432  brcup  24478  dfrdg4  24488  hfun  24808  anddi2  24941  ispridl2  26663  smprngopr  26677  isdmn3  26699  jm2.23  27089  aovov0bi  28056  prneimg  28073  ax12conj2  29108  a12study8  29119  a12peros  29121  4atlem3  29785  elpadd  29988  paddasslem17  30025  cdlemg31b0N  30883  cdlemg31b0a  30884  cdlemh  31006
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