Theorem orbi12i 915

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  pm4.78  935  andir  1011  anddi  1013  cases  1043  cases2  1048  3orbi123i  1157  3or6  1450  noran  1534  cadcoma  1614  eeor  2338  neorian  3027  sspsstri  4045  rexun  4136  elsymdif  4198  indi  4224  unabw  4247  unab  4248  dfnf5  4322  ab0orv  4323  inundif  4419  dfpr2  4588  ssunsn  4771  ssunpr  4777  sspr  4778  sstp  4779  prneimg  4797  prneimg2  4798  prnebg  4799  pwpr  4844  pwtp  4845  uniun  4873  iunun  5035  iunxun  5036  brun  5136  zfpair  5363  opthneg  5434  propeqop  5461  opthprc  5695  dmopab2rex  5872  xpeq0  6124  difxp  6128  ordtri2or3  6425  ftpg  7110  ordunpr  7777  xpord2pred  8095  xpord3pred  8102  mpoxneldm  8162  tpostpos  8196  frrlem13  8248  oarec  8497  brdom2  8929  modom  9161  dfsup2  9357  wemapsolem  9465  djuunxp  9845  leweon  9933  kmlem16  10088  fin23lem40  10273  axpre-lttri  11088  nn0n0n1ge2b  12506  elnn0z  12537  fz0  13493  sqeqori  14176  hashtpg  14447  swrdnnn0nd  14619  swrdnd0  14620  cbvsum  15657  cbvsumv  15658  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  rpnnen2lem12  16192  lcmfpr  16596  pythagtriplem2  16788  pythagtrip  16805  mreexexd  17614  smndex1basss  18876  smndex1mgm  18878  smndex1n0mnd  18883  opprdomnb  20694  cnfldfun  21366  ppttop  22972  fixufil  23887  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  dyaddisj  25563  noetalem1  27705  addsproplem2  27962  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  negsid  28033  mulsproplem9  28116  sltmuls1  28139  sltmuls2  28140  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  precsexlem9  28207  precsexlem11  28209  clwwlkneq0  30099  ofpreima2  32739  odutos  33028  trleile  33031  domnprodeq0  33337  prmidl2  33501  prmidl0  33510  smatrcl  33940  ordtconnlem1  34068  sitgaddlemb  34492  satfvsuclem2  35542  satfvsucsuc  35547  satfdm  35551  satf0  35554  satffunlem2lem1  35586  dmopab3rexdif  35587  quad3  35852  nepss  35900  dfso2  35937  dfon2lem4  35966  dfon2lem5  35967  dfon3  36072  brcup  36119  dfrdg4  36133  hfun  36360  sumeq2si  36384  prodeq2si  36386  cbvprodvw2  36429  bj-df-ifc  36845  bj-eltag  37284  bj-projun  37301  poimirlem22  37963  poimirlem31  37972  poimirlem32  37973  ispridl2  38359  smprngopr  38373  isdmn3  38395  sbcori  38430  tsbi4  38457  dfsucmap3  38784  4atlem3  40042  elpadd  40245  paddasslem17  40282  cdlemg31b0N  41140  cdlemg31b0a  41141  cdlemh  41263  jm2.23  43424  ifpim123g  43927  ifpananb  43933  rp-isfinite6  43945  iunrelexp0  44129  clsk1indlem3  44470  permaxinf2lem  45439  aovov0bi  47644  zeoALTV  48146  divgcdoddALTV  48158  clnbgrsym  48314  dfclnbgr6  48332  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  rrx2pnedifcoorneor  49192  line2xlem  49229