Theorem orbi12i 910

Description: Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
orbi12i.1	⊢ (𝜑 ↔ 𝜓)
orbi12i.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
orbi12i	⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
2	1	orbi2i 908	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 909	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 277	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  pm4.78  930  andir  1004  anddi  1006  cases  1036  cases2  1041  3orbi123i  1150  3or6  1440  noran  1519  noranOLD  1520  cadcoma  1606  neorian  3109  sspsstri  4077  rexun  4164  elsymdif  4222  indi  4248  unab  4268  dfnf5  4332  inundif  4425  dfpr2  4578  ssunsn  4753  ssunpr  4757  sspr  4758  sstp  4759  prneimg  4777  prnebg  4778  pwpr  4824  pwtp  4825  unipr  4843  uniun  4849  iunun  5006  iunxun  5007  brun  5108  zfpair  5312  opthneg  5364  propeqop  5388  pwunssOLD  5447  opthprc  5609  dmopab2rex  5779  xpeq0  6010  difxp  6014  ordtri2or3  6281  ftpg  6911  ordunpr  7533  mpoxneldm  7870  tpostpos  7904  oarec  8180  brdom2  8531  modom  8711  dfsup2  8900  wemapsolem  9006  djuunxp  9342  leweon  9429  kmlem16  9583  fin23lem40  9765  axpre-lttri  10579  nn0n0n1ge2b  11955  elnn0z  11986  fz0  12914  sqeqori  13568  hashtpg  13835  swrdnnn0nd  14010  swrdnd0  14011  cbvsum  15044  cbvprod  15261  rpnnen2lem12  15570  lcmfpr  15963  pythagtriplem2  16146  pythagtrip  16163  mreexexd  16911  smndex1basss  18062  smndex1mgm  18064  smndex1n0mnd  18069  cnfldfunALT  20550  ppttop  21607  fixufil  22522  alexsubALTlem2  22648  alexsubALTlem3  22649  alexsubALTlem4  22650  dyaddisj  24189  clwwlkneq0  27799  ofpreima2  30403  odutos  30643  trleile  30646  prmidl2  30951  smatrcl  31054  ordtconnlem1  31160  sitgaddlemb  31599  satfvsuclem2  32600  satfvsucsuc  32605  satfdm  32609  satf0  32612  satffunlem2lem1  32644  dmopab3rexdif  32645  quad3  32906  nepss  32941  dfso2  32983  dfon2lem4  33024  dfon2lem5  33025  frrlem13  33128  dfon3  33346  brcup  33393  dfrdg4  33405  hfun  33632  bj-df-ifc  33906  bj-eltag  34282  bj-projun  34299  poimirlem22  34906  poimirlem31  34915  poimirlem32  34916  ispridl2  35308  smprngopr  35322  isdmn3  35344  sbcori  35379  tsbi4  35406  4atlem3  36724  elpadd  36927  paddasslem17  36964  cdlemg31b0N  37822  cdlemg31b0a  37823  cdlemh  37945  jm2.23  39583  ifpim123g  39856  ifpananb  39862  rp-isfinite6  39874  iunrelexp0  40037  clsk1indlem3  40383  aovov0bi  43385  zeoALTV  43825  divgcdoddALTV  43837  rrx2pnedifcoorneor  44693  line2xlem  44730