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  3020  sspsstri  4058  rexun  4149  elsymdif  4211  indi  4237  unabw  4260  unab  4261  dfnf5  4335  ab0orv  4336  inundif  4432  dfpr2  4600  ssunsn  4782  ssunpr  4788  sspr  4789  sstp  4790  prneimg  4808  prneimg2  4809  prnebg  4810  pwpr  4855  pwtp  4856  uniun  4884  iunun  5045  iunxun  5046  brun  5146  zfpair  5363  opthneg  5428  propeqop  5454  opthprc  5687  dmopab2rex  5864  xpeq0  6113  difxp  6117  ordtri2or3  6413  ftpg  7094  ordunpr  7765  xpord2pred  8085  xpord3pred  8092  mpoxneldm  8152  tpostpos  8186  frrlem13  8238  oarec  8487  brdom2  8914  modom  9150  dfsup2  9353  wemapsolem  9461  djuunxp  9836  leweon  9924  kmlem16  10079  fin23lem40  10264  axpre-lttri  11078  nn0n0n1ge2b  12472  elnn0z  12503  fz0  13461  sqeqori  14140  hashtpg  14411  swrdnnn0nd  14582  swrdnd0  14583  cbvsum  15621  cbvsumv  15622  cbvprod  15839  cbvprodv  15840  prodeq1i  15842  rpnnen2lem12  16153  lcmfpr  16557  pythagtriplem2  16748  pythagtrip  16765  mreexexd  17573  smndex1basss  18798  smndex1mgm  18800  smndex1n0mnd  18805  opprdomnb  20621  cnfldfun  21294  cnfldfunOLD  21307  ppttop  22911  fixufil  23826  alexsubALTlem2  23952  alexsubALTlem3  23953  alexsubALTlem4  23954  dyaddisj  25514  noetalem1  27670  addsproplem2  27901  sleadd1  27920  addsuniflem  27932  addsasslem1  27934  addsasslem2  27935  negsid  27971  mulsproplem9  28051  ssltmul1  28074  ssltmul2  28075  addsdilem1  28078  addsdilem2  28079  mulsasslem1  28090  mulsasslem2  28091  precsexlem9  28141  precsexlem11  28143  clwwlkneq0  29992  ofpreima2  32628  odutos  32929  trleile  32932  prmidl2  33397  prmidl0  33406  smatrcl  33782  ordtconnlem1  33910  sitgaddlemb  34335  satfvsuclem2  35352  satfvsucsuc  35357  satfdm  35361  satf0  35364  satffunlem2lem1  35396  dmopab3rexdif  35397  quad3  35662  nepss  35710  dfso2  35747  dfon2lem4  35779  dfon2lem5  35780  dfon3  35885  brcup  35932  dfrdg4  35944  hfun  36171  sumeq2si  36195  prodeq2si  36197  cbvprodvw2  36240  bj-df-ifc  36573  bj-eltag  36970  bj-projun  36987  poimirlem22  37641  poimirlem31  37650  poimirlem32  37651  ispridl2  38037  smprngopr  38051  isdmn3  38073  sbcori  38108  tsbi4  38135  4atlem3  39595  elpadd  39798  paddasslem17  39835  cdlemg31b0N  40693  cdlemg31b0a  40694  cdlemh  40816  jm2.23  42989  ifpim123g  43493  ifpananb  43499  rp-isfinite6  43511  iunrelexp0  43695  clsk1indlem3  44036  permaxinf2lem  45006  aovov0bi  47200  zeoALTV  47674  divgcdoddALTV  47686  clnbgrsym  47842  dfclnbgr6  47860  usgrexmpl2nb0  48035  usgrexmpl2nb1  48036  usgrexmpl2nb2  48037  usgrexmpl2nb3  48038  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  usgrexmpl2trifr  48041  rrx2pnedifcoorneor  48721  line2xlem  48758