Theorem orbi12i 943

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

Syntax hints:   ↔ wb 198   ∨ wo 878

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 199  df-or 879

This theorem is referenced by:  pm4.78  963  andir  1036  anddi  1038  cases  1069  cases2  1074  3orbi123i  1199  3or6  1575  cadcoma  1725  neorian  3093  sspsstri  3937  rexun  4022  elsymdif  4077  symdif2OLD  4085  indi  4105  unab  4125  dfnf5  4184  inundif  4271  dfpr2  4418  ssunsn  4579  ssunpr  4583  sspr  4584  sstp  4585  prneimg  4605  prnebg  4606  pwpr  4654  pwtp  4655  unipr  4673  uniun  4681  iunun  4827  iunxun  4828  brun  4926  zfpair  5127  opthneg  5172  propeqop  5195  pwunss  5247  opthprc  5404  xpeq0  5799  difxp  5803  ordtri2or3  6064  ftpg  6679  ordunpr  7292  mpt2xneldm  7608  tpostpos  7642  oarec  7914  brdom2  8258  modom  8436  dfsup2  8625  wemapsolem  8731  djuunxp  9067  leweon  9154  kmlem16  9309  fin23lem40  9495  axpre-lttri  10309  nn0n0n1ge2b  11693  elnn0z  11724  fz0  12656  sqeqori  13277  hashtpg  13563  swrdnnn0nd  13728  swrdnd0  13729  cbvsum  14809  cbvprod  15025  rpnnen2lem12  15335  lcmfpr  15720  pythagtriplem2  15900  pythagtrip  15917  mreexexd  16668  cnfldfunALT  20126  ppttop  21189  fixufil  22103  alexsubALTlem2  22229  alexsubALTlem3  22230  alexsubALTlem4  22231  dyaddisj  23769  clwwlkneq0  27374  ofpreima2  30011  odutos  30204  trleile  30207  smatrcl  30403  ordtconnlem1  30511  sitgaddlemb  30951  quad3  32104  nepss  32139  dfso2  32182  dfon2lem4  32224  dfon2lem5  32225  dfon3  32533  brcup  32580  dfrdg4  32592  hfun  32819  bj-dfifc2  33088  bj-eltag  33486  bj-projun  33503  bj-ismooredr2  33587  poimirlem22  33974  poimirlem31  33983  poimirlem32  33984  ispridl2  34378  smprngopr  34392  isdmn3  34414  sbcori  34451  tsbi4  34482  4atlem3  35670  elpadd  35873  paddasslem17  35910  cdlemg31b0N  36768  cdlemg31b0a  36769  cdlemh  36891  jm2.23  38405  ifpim123g  38686  ifpananb  38692  rp-isfinite6  38704  iunrelexp0  38834  clsk1indlem3  39180  aovov0bi  42096  zeoALTV  42429  divgcdoddALTV  42441  line2xlem  43319