Theorem orbi12i 927

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  pm4.78  947  andir  1024  anddi  1026  cases  1056  cases2  1061  3orbi123i  1172  3or6  1473  noran  1559  cadcoma  1639  eeor  2372  neorian  3059  sspsstri  4068  rexun  4157  elsymdif  4219  indi  4245  unabw  4268  unab  4269  dfnf5  4345  ab0orv  4346  inundif  4445  dfpr2  4615  ssunsn  4798  ssunpr  4803  sspr  4804  sstp  4805  prneimg  4823  prneimg2  4824  prnebg  4825  pwpr  4870  pwtp  4871  uniun  4899  iunun  5063  iunxun  5064  brun  5166  zfpair  5393  opthneg  5464  propeqop  5491  opthprc  5726  dmopab2rex  5908  xpeq0  6158  difxp  6162  ordtri2or3  6464  ftpg  7154  ordunpr  7821  xpord2pred  8140  xpord3pred  8147  mpoxneldm  8207  tpostpos  8241  frrlem13  8294  oarec  8546  brdom2  8978  modom  9210  dfsup2  9403  wemapsolem  9511  djuunxp  9906  leweon  9994  kmlem16  10148  fin23lem40  10334  axpre-lttri  11149  nn0n0n1ge2b  12572  elnn0z  12603  fz0  13566  sqeqori  14249  hashtpg  14521  swrdnnn0nd  14693  swrdnd0  14694  cbvsum  15745  cbvsumv  15746  cbvprod  15966  cbvprodv  15967  prodeq1i  15969  rpnnen2lem12  16280  lcmfpr  16684  pythagtriplem2  16876  pythagtrip  16893  mreexexd  17703  smndex1basss  18966  smndex1mgm  18968  smndex1n0mnd  18973  opprdomnb  20800  prmidl2  21436  prmidl0  21446  cnfldfun  21504  ppttop  23132  fixufil  24047  alexsubALTlem2  24173  alexsubALTlem3  24174  alexsubALTlem4  24175  dyaddisj  25723  noetalem1  27870  addsproplem2  28128  leadds1  28147  addsuniflem  28159  addsasslem1  28161  addsasslem2  28162  negsid  28199  mulsproplem9  28282  sltmuls1  28305  sltmuls2  28306  addsdilem1  28309  addsdilem2  28310  mulsasslem1  28321  mulsasslem2  28322  precsexlem9  28373  precsexlem11  28375  clwwlkneq0  30320  ofpreima2  32951  odutos  33228  trleile  33231  domnprodeq0  33539  smatrcl  34130  ordtconnlem1  34258  sitgaddlemb  34682  satfvsuclem2  35750  satfvsucsuc  35755  satfdm  35759  satf0  35762  satffunlem2lem1  35794  dmopab3rexdif  35795  quad3  36060  nepss  36108  dfso2  36145  dfon2lem4  36174  dfon2lem5  36175  dfon3  36280  brcup  36327  dfrdg4  36341  hfun  36568  sumeq2si  36602  prodeq2si  36604  cbvprodvw2  36647  bj-df-ifc  37061  bj-eltag  37500  bj-projun  37517  poimirlem22  38180  poimirlem31  38189  poimirlem32  38190  ispridl2  38576  smprngopr  38590  isdmn3  38612  sbcori  38647  tsbi4  38674  dfsucmap3  39001  4atlem3  40259  elpadd  40462  paddasslem17  40499  cdlemg31b0N  41357  cdlemg31b0a  41358  cdlemh  41480  jm2.23  43614  ifpim123g  44117  ifpananb  44123  rp-isfinite6  44135  iunrelexp0  44319  clsk1indlem3  44660  permaxinf2lem  45612  aovov0bi  47821  zeoALTV  48323  divgcdoddALTV  48335  clnbgrsym  48491  dfclnbgr6  48509  usgrexmpl2nb0  48684  usgrexmpl2nb1  48685  usgrexmpl2nb2  48686  usgrexmpl2nb3  48687  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  usgrexmpl2trifr  48690  smprngprmrng  48992  rrx2pnedifcoorneor  49380  line2xlem  49417