Theorem orbi12i 928

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 926	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 927	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 278	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.78  948  andir  1026  anddi  1028  cases  1058  cases2  1063  3orbi123i  1174  3or6  1476  noran  1562  cadcoma  1645  eeor  2363  neorian  3050  sspsstri  4054  rexun  4142  elsymdif  4204  indi  4230  unabw  4253  unab  4254  dfnf5  4331  ab0orv  4332  inundif  4435  dfpr2  4605  ssunsn  4789  ssunpr  4794  sspr  4795  sstp  4796  prneimg  4814  prneimg2  4815  prnebg  4816  pwpr  4861  pwtp  4862  uniun  4890  iunun  5053  iunxun  5054  brun  5156  zfpair  5386  opthneg  5457  propeqop  5484  opthprc  5719  dmopab2rex  5901  xpeq0  6152  difxp  6156  ordtri2or3  6460  ftpg  7154  ordunpr  7823  xpord2pred  8144  xpord3pred  8151  mpoxneldm  8211  tpostpos  8245  frrlem13  8298  oarec  8550  brdom2  8989  modom  9222  dfsup2  9415  wemapsolem  9523  djuunxp  9927  leweon  10015  kmlem16  10169  fin23lem40  10354  axpre-lttri  11175  nn0n0n1ge2b  12598  elnn0z  12629  fz0  13594  sqeqori  14279  hashtpg  14551  swrdnnn0nd  14727  swrdnd0  14728  cbvsum  15783  cbvsumv  15784  cbvprod  16003  cbvprodv  16004  prodeq1i  16006  rpnnen2lem12  16314  lcmfpr  16718  pythagtriplem2  16910  pythagtrip  16927  mreexexd  17737  smndex1basss  19018  smndex1mgm  19020  smndex1n0mnd  19025  opprdomnb  20879  prmidl2  21530  prmidl0  21542  cnfldfun  21600  ppttop  23233  fixufil  24149  alexsubALTlem2  24275  alexsubALTlem3  24276  alexsubALTlem4  24277  dyaddisj  25825  noetalem1  27978  addsproplem2  28236  leadds1  28255  addsuniflem  28267  addsasslem1  28269  addsasslem2  28270  negsid  28307  mulsproplem9  28390  sltmuls1  28413  sltmuls2  28414  addsdilem1  28417  addsdilem2  28418  mulsasslem1  28429  mulsasslem2  28430  precsexlem9  28481  precsexlem11  28483  clwwlkneq0  30500  ofpreima2  33140  odutos  33409  trleile  33412  domnprodeq0  33720  smatrcl  34307  ordtconnlem1  34435  sitgaddlemb  34860  satfvsuclem2  35940  satfvsucsuc  35945  satfdm  35949  satf0  35952  satffunlem2lem1  35984  dmopab3rexdif  35985  quad3  36250  nepss  36298  dfso2  36335  dfon2lem4  36364  dfon2lem5  36365  dfon3  36470  brcup  36517  dfrdg4  36531  hfun  36759  ltnadd  36799  naddle  36800  sumeq2si  36823  prodeq2si  36825  cbvprodvw2  36868  bj-df-ifc  37282  bj-eltag  37722  bj-projun  37739  poimirlem22  38392  poimirlem31  38401  poimirlem32  38402  ispridl2  38789  smprngopr  38803  isdmn3  38825  sbcori  38858  tsbi4  38885  dfsucmap3  39212  4atlem3  40470  elpadd  40673  paddasslem17  40710  cdlemg31b0N  41568  cdlemg31b0a  41569  cdlemh  41691  jm2.23  43838  ifpim123g  44341  ifpananb  44347  rp-isfinite6  44359  iunrelexp0  44543  clsk1indlem3  44884  permaxinf2lem  45836  aovov0bi  48085  zeoALTV  48587  divgcdoddALTV  48599  clnbgrsym  48755  dfclnbgr6  48773  usgrexmpl2nb0  48948  usgrexmpl2nb1  48949  usgrexmpl2nb2  48950  usgrexmpl2nb3  48951  usgrexmpl2nb4  48952  usgrexmpl2nb5  48953  usgrexmpl2trifr  48954  smprngprmrng  49255  isidom3  49261  rrx2pnedifcoorneor  49647  line2xlem  49684