Theorem orbi12i 921

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

Syntax hints:   ↔ wb 208   ∨ wo 854

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 855

This theorem is referenced by:  pm4.78  941  andir  1017  anddi  1019  cases  1049  cases2  1054  3orbi123i  1163  3or6  1456  noran  1540  cadcoma  1620  eeor  2344  neorian  3031  sspsstri  4039  rexun  4128  elsymdif  4189  indi  4215  unabw  4238  unab  4239  dfnf5  4313  ab0orv  4314  inundif  4410  dfpr2  4579  ssunsn  4762  ssunpr  4768  sspr  4769  sstp  4770  prneimg  4788  prneimg2  4789  prnebg  4790  pwpr  4835  pwtp  4836  uniun  4864  iunun  5025  iunxun  5026  brun  5126  zfpair  5353  opthneg  5424  propeqop  5451  opthprc  5685  dmopab2rex  5866  xpeq0  6115  difxp  6119  ordtri2or3  6416  ftpg  7103  ordunpr  7770  xpord2pred  8089  xpord3pred  8096  mpoxneldm  8156  tpostpos  8190  frrlem13  8242  oarec  8491  brdom2  8923  modom  9155  dfsup2  9351  wemapsolem  9459  djuunxp  9840  leweon  9928  kmlem16  10083  fin23lem40  10268  axpre-lttri  11083  nn0n0n1ge2b  12501  elnn0z  12532  fz0  13488  sqeqori  14171  hashtpg  14442  swrdnnn0nd  14614  swrdnd0  14615  cbvsum  15652  cbvsumv  15653  cbvprod  15873  cbvprodv  15874  prodeq1i  15876  rpnnen2lem12  16187  lcmfpr  16591  pythagtriplem2  16783  pythagtrip  16800  mreexexd  17609  smndex1basss  18871  smndex1mgm  18873  smndex1n0mnd  18878  opprdomnb  20693  cnfldfun  21365  ppttop  22994  fixufil  23909  alexsubALTlem2  24035  alexsubALTlem3  24036  alexsubALTlem4  24037  dyaddisj  25585  noetalem1  27727  addsproplem2  27984  leadds1  28003  addsuniflem  28015  addsasslem1  28017  addsasslem2  28018  negsid  28055  mulsproplem9  28138  sltmuls1  28161  sltmuls2  28162  addsdilem1  28165  addsdilem2  28166  mulsasslem1  28177  mulsasslem2  28178  precsexlem9  28229  precsexlem11  28231  clwwlkneq0  30121  ofpreima2  32762  odutos  33051  trleile  33054  domnprodeq0  33361  prmidl2  33528  prmidl0  33537  smatrcl  33992  ordtconnlem1  34120  sitgaddlemb  34544  satfvsuclem2  35603  satfvsucsuc  35608  satfdm  35612  satf0  35615  satffunlem2lem1  35647  dmopab3rexdif  35648  quad3  35913  nepss  35961  dfso2  35998  dfon2lem4  36027  dfon2lem5  36028  dfon3  36133  brcup  36180  dfrdg4  36194  hfun  36421  sumeq2si  36445  prodeq2si  36447  cbvprodvw2  36490  bj-df-ifc  36906  bj-eltag  37345  bj-projun  37362  poimirlem22  38024  poimirlem31  38033  poimirlem32  38034  ispridl2  38420  smprngopr  38434  isdmn3  38456  sbcori  38491  tsbi4  38518  dfsucmap3  38845  4atlem3  40103  elpadd  40306  paddasslem17  40343  cdlemg31b0N  41201  cdlemg31b0a  41202  cdlemh  41324  jm2.23  43456  ifpim123g  43959  ifpananb  43965  rp-isfinite6  43977  iunrelexp0  44161  clsk1indlem3  44502  permaxinf2lem  45471  aovov0bi  47673  zeoALTV  48175  divgcdoddALTV  48187  clnbgrsym  48343  dfclnbgr6  48361  usgrexmpl2nb0  48536  usgrexmpl2nb1  48537  usgrexmpl2nb2  48538  usgrexmpl2nb3  48539  usgrexmpl2nb4  48540  usgrexmpl2nb5  48541  usgrexmpl2trifr  48542  rrx2pnedifcoorneor  49221  line2xlem  49258