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  866  anddi  868  dfbi3  891  4exmid  937  cases  969  3orbi123i  1186  3or6  1310  cadcoma  1447  neorian  2794  sspsstri  3606  rexun  3684  indi  3744  symdif2  3764  unab  3765  inundif  3905  dfpr2  4042  ssunsn  4187  ssunpr  4189  sspr  4190  sstp  4191  prneimg  4207  prnebg  4208  pwpr  4241  pwtp  4242  unipr  4258  uniun  4264  iunun  4406  iunxun  4407  brun  4495  zfpair  4684  pwunss  4785  ordtri2or3  4975  opthprc  5047  xpeq0  5427  difxp  5431  ftpg  6072  ordunpr  6646  tpostpos  6976  oarec  7212  brdom2  7546  modom  7721  dfsup2  7903  wemapsolem  7976  leweon  8390  kmlem16  8546  fin23lem40  8732  axpre-lttri  9543  nn0n0n1ge2b  10861  elnn0z  10878  fz0  11702  sqeqori  12249  hashtpg  12490  cbvsum  13483  rpnnen2  13823  pythagtriplem2  14203  pythagtrip  14220  mreexexd  14906  ppttop  19314  fixufil  20250  alexsubALTlem2  20375  alexsubALTlem3  20376  alexsubALTlem4  20377  dyaddisj  21832  elim2if  27193  ofpreima2  27277  odutos  27410  trleile  27413  ordtconlem1  27657  quad3  28775  nepss  28846  cbvprod  28900  dfso2  29036  dfon2lem4  29071  dfon2lem5  29072  nofulllem5  29319  elsymdif  29326  dfon3  29395  brcup  29442  dfrdg4  29453  hfun  29688  ispridl2  30265  smprngopr  30279  isdmn3  30301  sbcori  30341  jm2.23  30769  aovov0bi  31975  bj-dfifc2  33462  bj-eltag  33833  bj-projun  33850  4atlem3  34609  elpadd  34812  paddasslem17  34849  cdlemg31b0N  35707  cdlemg31b0a  35708  cdlemh  35830
  Copyright terms: Public domain W3C validator