Theorem orbi12i 543

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

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3 |- ( ch <-> th )
2	1	orbi2i 541	. 2 |- ( ( ph \/ ch ) <-> ( ph \/ th ) )
3		orbi12i.1	. . 3 |- ( ph <-> ps )
4	3	orbi1i 542	. 2 |- ( ( ph \/ th ) <-> ( ps \/ th ) )
5	2, 4	bitri 264	1 |- ( ( ph \/ ch ) <-> ( ps \/ th ) )

Syntax hints:   <-> wb 196   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  pm4.78  606  andir  912  anddi  914  cases  992  dfbi3OLD  995  4exmidOLD  998  3orbi123i  1252  3or6  1410  cadcoma  1551  neorian  2888  sspsstri  3709  rexun  3793  elsymdif  3849  symdif2  3852  indi  3873  unab  3894  dfnf5  3952  inundif  4046  dfpr2  4195  ssunsn  4360  ssunpr  4365  sspr  4366  sstp  4367  prneimg  4388  prnebg  4389  pwpr  4430  pwtp  4431  unipr  4449  uniun  4456  iunun  4604  iunxun  4605  brun  4703  zfpair  4904  opthneg  4950  propeqop  4970  pwunss  5019  opthprc  5167  xpeq0  5554  difxp  5558  ordtri2or3  5824  ftpg  6423  ordunpr  7026  mpt2xneldm  7338  tpostpos  7372  oarec  7642  brdom2  7985  modom  8161  dfsup2  8350  wemapsolem  8455  leweon  8834  kmlem16  8987  fin23lem40  9173  axpre-lttri  9986  nn0n0n1ge2b  11359  elnn0z  11390  fz0  12356  sqeqori  12976  hashtpg  13267  cbvsum  14425  cbvprod  14645  rpnnen2lem12  14954  lcmfpr  15340  pythagtriplem2  15522  pythagtrip  15539  mreexexd  16308  mreexexdOLD  16309  cnfldfunALT  19759  ppttop  20811  fixufil  21726  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  dyaddisj  23364  ofpreima2  29466  odutos  29663  trleile  29666  smatrcl  29862  ordtconnlem1  29970  sitgaddlemb  30410  quad3  31564  nepss  31599  dfso2  31644  dfon2lem4  31691  dfon2lem5  31692  dfon3  31999  brcup  32046  dfrdg4  32058  hfun  32285  bj-dfifc2  32564  bj-eltag  32965  bj-projun  32982  bj-ismooredr2  33065  poimirlem22  33431  poimirlem31  33440  poimirlem32  33441  ispridl2  33837  smprngopr  33851  isdmn3  33873  sbcori  33911  tsbi4  33943  4atlem3  34882  elpadd  35085  paddasslem17  35122  cdlemg31b0N  35982  cdlemg31b0a  35983  cdlemh  36105  jm2.23  37563  ifpim123g  37845  ifpananb  37851  rp-isfinite6  37864  iunrelexp0  37994  clsk1indlem3  38341  aovov0bi  41276  zeoALTV  41581  divgcdoddALTV  41593