Theorem orbi12i 915

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  pm4.78  935  andir  1011  anddi  1013  cases  1043  cases2  1048  3orbi123i  1157  3or6  1450  noran  1534  cadcoma  1614  eeor  2339  neorian  3028  sspsstri  4046  rexun  4137  elsymdif  4199  indi  4225  unabw  4248  unab  4249  dfnf5  4323  ab0orv  4324  inundif  4420  dfpr2  4589  ssunsn  4772  ssunpr  4778  sspr  4779  sstp  4780  prneimg  4798  prneimg2  4799  prnebg  4800  pwpr  4845  pwtp  4846  uniun  4874  iunun  5036  iunxun  5037  brun  5137  zfpair  5359  opthneg  5430  propeqop  5456  opthprc  5689  dmopab2rex  5867  xpeq0  6119  difxp  6123  ordtri2or3  6420  ftpg  7104  ordunpr  7771  xpord2pred  8089  xpord3pred  8096  mpoxneldm  8156  tpostpos  8190  frrlem13  8242  oarec  8491  brdom2  8923  modom  9155  dfsup2  9351  wemapsolem  9459  djuunxp  9839  leweon  9927  kmlem16  10082  fin23lem40  10267  axpre-lttri  11082  nn0n0n1ge2b  12500  elnn0z  12531  fz0  13487  sqeqori  14170  hashtpg  14441  swrdnnn0nd  14613  swrdnd0  14614  cbvsum  15651  cbvsumv  15652  cbvprod  15872  cbvprodv  15873  prodeq1i  15875  rpnnen2lem12  16186  lcmfpr  16590  pythagtriplem2  16782  pythagtrip  16799  mreexexd  17608  smndex1basss  18870  smndex1mgm  18872  smndex1n0mnd  18877  opprdomnb  20688  cnfldfun  21361  cnfldfunOLD  21374  ppttop  22985  fixufil  23900  alexsubALTlem2  24026  alexsubALTlem3  24027  alexsubALTlem4  24028  dyaddisj  25576  noetalem1  27722  addsproplem2  27979  leadds1  27998  addsuniflem  28010  addsasslem1  28012  addsasslem2  28013  negsid  28050  mulsproplem9  28133  sltmuls1  28156  sltmuls2  28157  addsdilem1  28160  addsdilem2  28161  mulsasslem1  28172  mulsasslem2  28173  precsexlem9  28224  precsexlem11  28226  clwwlkneq0  30117  ofpreima2  32757  odutos  33046  trleile  33049  domnprodeq0  33355  prmidl2  33519  prmidl0  33528  smatrcl  33959  ordtconnlem1  34087  sitgaddlemb  34511  satfvsuclem2  35561  satfvsucsuc  35566  satfdm  35570  satf0  35573  satffunlem2lem1  35605  dmopab3rexdif  35606  quad3  35871  nepss  35919  dfso2  35956  dfon2lem4  35985  dfon2lem5  35986  dfon3  36091  brcup  36138  dfrdg4  36152  hfun  36379  sumeq2si  36403  prodeq2si  36405  cbvprodvw2  36448  bj-df-ifc  36864  bj-eltag  37303  bj-projun  37320  poimirlem22  37980  poimirlem31  37989  poimirlem32  37990  ispridl2  38376  smprngopr  38390  isdmn3  38412  sbcori  38447  tsbi4  38474  dfsucmap3  38801  4atlem3  40059  elpadd  40262  paddasslem17  40299  cdlemg31b0N  41157  cdlemg31b0a  41158  cdlemh  41280  jm2.23  43445  ifpim123g  43948  ifpananb  43954  rp-isfinite6  43966  iunrelexp0  44150  clsk1indlem3  44491  permaxinf2lem  45460  aovov0bi  47659  zeoALTV  48161  divgcdoddALTV  48173  clnbgrsym  48329  dfclnbgr6  48347  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  rrx2pnedifcoorneor  49207  line2xlem  49244