Theorem orbi12i 914

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  pm4.78  934  andir  1010  anddi  1012  cases  1042  cases2  1047  3orbi123i  1156  3or6  1449  noran  1532  cadcoma  1612  eeor  2332  neorian  3021  sspsstri  4071  rexun  4162  elsymdif  4224  indi  4250  unabw  4273  unab  4274  dfnf5  4348  ab0orv  4349  inundif  4445  dfpr2  4613  ssunsn  4795  ssunpr  4801  sspr  4802  sstp  4803  prneimg  4821  prneimg2  4822  prnebg  4823  pwpr  4868  pwtp  4869  uniun  4897  iunun  5060  iunxun  5061  brun  5161  zfpair  5379  opthneg  5444  propeqop  5470  opthprc  5705  dmopab2rex  5884  xpeq0  6136  difxp  6140  ordtri2or3  6437  ftpg  7131  ordunpr  7804  xpord2pred  8127  xpord3pred  8134  mpoxneldm  8194  tpostpos  8228  frrlem13  8280  oarec  8529  brdom2  8956  modom  9198  dfsup2  9402  wemapsolem  9510  djuunxp  9881  leweon  9971  kmlem16  10126  fin23lem40  10311  axpre-lttri  11125  nn0n0n1ge2b  12518  elnn0z  12549  fz0  13507  sqeqori  14186  hashtpg  14457  swrdnnn0nd  14628  swrdnd0  14629  cbvsum  15668  cbvsumv  15669  cbvprod  15886  cbvprodv  15887  prodeq1i  15889  rpnnen2lem12  16200  lcmfpr  16604  pythagtriplem2  16795  pythagtrip  16812  mreexexd  17616  smndex1basss  18839  smndex1mgm  18841  smndex1n0mnd  18846  opprdomnb  20633  cnfldfun  21285  cnfldfunOLD  21298  ppttop  22901  fixufil  23816  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  dyaddisj  25504  noetalem1  27660  addsproplem2  27884  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  negsid  27954  mulsproplem9  28034  ssltmul1  28057  ssltmul2  28058  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  precsexlem9  28124  precsexlem11  28126  clwwlkneq0  29965  ofpreima2  32597  odutos  32901  trleile  32904  prmidl2  33419  prmidl0  33428  smatrcl  33793  ordtconnlem1  33921  sitgaddlemb  34346  satfvsuclem2  35354  satfvsucsuc  35359  satfdm  35363  satf0  35366  satffunlem2lem1  35398  dmopab3rexdif  35399  quad3  35664  nepss  35712  dfso2  35749  dfon2lem4  35781  dfon2lem5  35782  dfon3  35887  brcup  35934  dfrdg4  35946  hfun  36173  sumeq2si  36197  prodeq2si  36199  cbvprodvw2  36242  bj-df-ifc  36575  bj-eltag  36972  bj-projun  36989  poimirlem22  37643  poimirlem31  37652  poimirlem32  37653  ispridl2  38039  smprngopr  38053  isdmn3  38075  sbcori  38110  tsbi4  38137  4atlem3  39597  elpadd  39800  paddasslem17  39837  cdlemg31b0N  40695  cdlemg31b0a  40696  cdlemh  40818  jm2.23  42992  ifpim123g  43496  ifpananb  43502  rp-isfinite6  43514  iunrelexp0  43698  clsk1indlem3  44039  permaxinf2lem  45009  aovov0bi  47201  zeoALTV  47675  divgcdoddALTV  47687  clnbgrsym  47842  dfclnbgr6  47860  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  rrx2pnedifcoorneor  48709  line2xlem  48746