Theorem orbi12i 920

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

Syntax hints:   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm4.78  940  andir  1016  anddi  1018  cases  1048  cases2  1053  3orbi123i  1162  3or6  1455  noran  1539  cadcoma  1619  eeor  2342  neorian  3029  sspsstri  4036  rexun  4125  elsymdif  4186  indi  4212  unabw  4235  unab  4236  dfnf5  4310  ab0orv  4311  inundif  4407  dfpr2  4576  ssunsn  4759  ssunpr  4765  sspr  4766  sstp  4767  prneimg  4785  prneimg2  4786  prnebg  4787  pwpr  4832  pwtp  4833  uniun  4861  iunun  5022  iunxun  5023  brun  5123  zfpair  5350  opthneg  5421  propeqop  5448  opthprc  5682  dmopab2rex  5859  xpeq0  6111  difxp  6115  ordtri2or3  6412  ftpg  7099  ordunpr  7766  xpord2pred  8085  xpord3pred  8092  mpoxneldm  8152  tpostpos  8186  frrlem13  8238  oarec  8487  brdom2  8919  modom  9151  dfsup2  9347  wemapsolem  9455  djuunxp  9836  leweon  9924  kmlem16  10079  fin23lem40  10264  axpre-lttri  11079  nn0n0n1ge2b  12497  elnn0z  12528  fz0  13484  sqeqori  14167  hashtpg  14438  swrdnnn0nd  14610  swrdnd0  14611  cbvsum  15648  cbvsumv  15649  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  rpnnen2lem12  16183  lcmfpr  16587  pythagtriplem2  16779  pythagtrip  16796  mreexexd  17605  smndex1basss  18867  smndex1mgm  18869  smndex1n0mnd  18874  opprdomnb  20689  cnfldfun  21361  ppttop  22990  fixufil  23905  alexsubALTlem2  24031  alexsubALTlem3  24032  alexsubALTlem4  24033  dyaddisj  25581  noetalem1  27723  addsproplem2  27980  leadds1  27999  addsuniflem  28011  addsasslem1  28013  addsasslem2  28014  negsid  28051  mulsproplem9  28134  sltmuls1  28157  sltmuls2  28158  addsdilem1  28161  addsdilem2  28162  mulsasslem1  28173  mulsasslem2  28174  precsexlem9  28225  precsexlem11  28227  clwwlkneq0  30117  ofpreima2  32758  odutos  33047  trleile  33050  domnprodeq0  33357  prmidl2  33524  prmidl0  33533  smatrcl  33980  ordtconnlem1  34108  sitgaddlemb  34532  satfvsuclem2  35588  satfvsucsuc  35593  satfdm  35597  satf0  35600  satffunlem2lem1  35632  dmopab3rexdif  35633  quad3  35898  nepss  35946  dfso2  35983  dfon2lem4  36012  dfon2lem5  36013  dfon3  36118  brcup  36165  dfrdg4  36179  hfun  36406  sumeq2si  36430  prodeq2si  36432  cbvprodvw2  36475  bj-df-ifc  36891  bj-eltag  37330  bj-projun  37347  poimirlem22  38009  poimirlem31  38018  poimirlem32  38019  ispridl2  38405  smprngopr  38419  isdmn3  38441  sbcori  38476  tsbi4  38503  dfsucmap3  38830  4atlem3  40088  elpadd  40291  paddasslem17  40328  cdlemg31b0N  41186  cdlemg31b0a  41187  cdlemh  41309  jm2.23  43441  ifpim123g  43944  ifpananb  43950  rp-isfinite6  43962  iunrelexp0  44146  clsk1indlem3  44487  permaxinf2lem  45456  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