Theorem orbi12i 911

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

Syntax hints:   ↔ wb 208   ∨ wo 843

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 844

This theorem is referenced by:  pm4.78  931  andir  1005  anddi  1007  cases  1037  cases2  1042  3orbi123i  1152  3or6  1443  noran  1526  noranOLD  1527  cadcoma  1613  neorian  3113  sspsstri  4081  rexun  4168  elsymdif  4226  indi  4252  unab  4272  dfnf5  4336  inundif  4429  dfpr2  4588  ssunsn  4763  ssunpr  4767  sspr  4768  sstp  4769  prneimg  4787  prnebg  4788  pwpr  4834  pwtp  4835  unipr  4857  uniun  4863  iunun  5017  iunxun  5018  brun  5119  zfpair  5324  opthneg  5375  propeqop  5399  pwunssOLD  5457  opthprc  5618  dmopab2rex  5788  xpeq0  6019  difxp  6023  ordtri2or3  6290  ftpg  6920  ordunpr  7543  mpoxneldm  7880  tpostpos  7914  oarec  8190  brdom2  8541  modom  8721  dfsup2  8910  wemapsolem  9016  djuunxp  9352  leweon  9439  kmlem16  9593  fin23lem40  9775  axpre-lttri  10589  nn0n0n1ge2b  11966  elnn0z  11997  fz0  12925  sqeqori  13579  hashtpg  13846  swrdnnn0nd  14020  swrdnd0  14021  cbvsum  15054  cbvprod  15271  rpnnen2lem12  15580  lcmfpr  15973  pythagtriplem2  16156  pythagtrip  16173  mreexexd  16921  smndex1basss  18072  smndex1mgm  18074  smndex1n0mnd  18079  cnfldfunALT  20560  ppttop  21617  fixufil  22532  alexsubALTlem2  22658  alexsubALTlem3  22659  alexsubALTlem4  22660  dyaddisj  24199  clwwlkneq0  27809  ofpreima2  30413  odutos  30652  trleile  30655  prmidl2  30960  smatrcl  31063  ordtconnlem1  31169  sitgaddlemb  31608  satfvsuclem2  32609  satfvsucsuc  32614  satfdm  32618  satf0  32621  satffunlem2lem1  32653  dmopab3rexdif  32654  quad3  32915  nepss  32950  dfso2  32992  dfon2lem4  33033  dfon2lem5  33034  frrlem13  33137  dfon3  33355  brcup  33402  dfrdg4  33414  hfun  33641  bj-df-ifc  33915  bj-eltag  34291  bj-projun  34308  poimirlem22  34916  poimirlem31  34925  poimirlem32  34926  ispridl2  35318  smprngopr  35332  isdmn3  35354  sbcori  35389  tsbi4  35416  4atlem3  36734  elpadd  36937  paddasslem17  36974  cdlemg31b0N  37832  cdlemg31b0a  37833  cdlemh  37955  jm2.23  39600  ifpim123g  39873  ifpananb  39879  rp-isfinite6  39891  iunrelexp0  40054  clsk1indlem3  40400  aovov0bi  43402  zeoALTV  43842  divgcdoddALTV  43854  rrx2pnedifcoorneor  44710  line2xlem  44747