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

Theorem orbi12i 524
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 522 . 2  |-  ( (
ph  \/  ch )  <->  (
ph  \/  th )
)
3 orbi12i.1 . . 3  |-  ( ph  <->  ps )
43orbi1i 523 . 2  |-  ( (
ph  \/  th )  <->  ( ps  \/  th )
)
52, 4bitri 253 1  |-  ( (
ph  \/  ch )  <->  ( ps  \/  th )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  pm4.78  586  andir  879  anddi  881  dfbi3  904  4exmid  950  cases  982  3orbi123i  1198  3or6  1350  cadcoma  1515  neorian  2718  sspsstri  3535  rexun  3614  elsymdif  3668  symdif2  3671  indi  3689  unab  3710  inundif  3845  dfpr2  3983  ssunsn  4132  ssunpr  4134  sspr  4135  sstp  4136  prneimg  4156  prnebg  4157  pwpr  4194  pwtp  4195  unipr  4211  uniun  4217  iunun  4362  iunxun  4363  brun  4451  zfpair  4637  pwunss  4739  opthprc  4882  xpeq0  5257  difxp  5261  ordtri2or3  5520  ftpg  6074  ordunpr  6653  mpt2xneldm  6958  tpostpos  6993  oarec  7263  brdom2  7599  modom  7773  dfsup2  7958  wemapsolem  8065  leweon  8442  kmlem16  8595  fin23lem40  8781  axpre-lttri  9589  nn0n0n1ge2b  10933  elnn0z  10950  fz0  11814  sqeqori  12386  hashtpg  12641  cbvsum  13761  cbvprod  13969  rpnnen2  14278  lcmfpr  14600  pythagtriplem2  14767  pythagtrip  14784  mreexexd  15554  ppttop  20022  fixufil  20937  alexsubALTlem2  21063  alexsubALTlem3  21064  alexsubALTlem4  21065  dyaddisj  22554  ofpreima2  28269  odutos  28424  trleile  28427  smatrcl  28622  ordtconlem1  28730  sitgaddlemb  29181  quad3  30302  nepss  30350  dfso2  30394  dfon2lem4  30432  dfon2lem5  30433  nofulllem5  30595  dfon3  30659  brcup  30706  dfrdg4  30718  hfun  30945  bj-dfifc2  31158  bj-eltag  31571  bj-projun  31588  poimirlem22  31962  poimirlem31  31971  poimirlem32  31972  ispridl2  32271  smprngopr  32285  isdmn3  32307  sbcori  32346  tsbi4  32378  4atlem3  33161  elpadd  33364  paddasslem17  33401  cdlemg31b0N  34261  cdlemg31b0a  34262  cdlemh  34384  jm2.23  35851  ifpim123g  36144  ifpananb  36150  rp-isfinite6  36163  iunrelexp0  36294  aovov0bi  38698  zeoALTV  38799  divgcdoddALTV  38811  propeqop  38999
  Copyright terms: Public domain W3C validator