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  2339  neorian  3028  sspsstri  4059  rexun  4150  elsymdif  4212  indi  4238  unabw  4261  unab  4262  dfnf5  4336  ab0orv  4337  inundif  4433  dfpr2  4603  ssunsn  4786  ssunpr  4792  sspr  4793  sstp  4794  prneimg  4812  prneimg2  4813  prnebg  4814  pwpr  4859  pwtp  4860  uniun  4888  iunun  5050  iunxun  5051  brun  5151  zfpair  5368  opthneg  5437  propeqop  5463  opthprc  5696  dmopab2rex  5874  xpeq0  6126  difxp  6130  ordtri2or3  6427  ftpg  7111  ordunpr  7778  xpord2pred  8097  xpord3pred  8104  mpoxneldm  8164  tpostpos  8198  frrlem13  8250  oarec  8499  brdom2  8931  modom  9163  dfsup2  9359  wemapsolem  9467  djuunxp  9845  leweon  9933  kmlem16  10088  fin23lem40  10273  axpre-lttri  11088  nn0n0n1ge2b  12482  elnn0z  12513  fz0  13467  sqeqori  14149  hashtpg  14420  swrdnnn0nd  14592  swrdnd0  14593  cbvsum  15630  cbvsumv  15631  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  rpnnen2lem12  16162  lcmfpr  16566  pythagtriplem2  16757  pythagtrip  16774  mreexexd  17583  smndex1basss  18842  smndex1mgm  18844  smndex1n0mnd  18849  opprdomnb  20662  cnfldfun  21335  cnfldfunOLD  21348  ppttop  22963  fixufil  23878  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  dyaddisj  25565  noetalem1  27721  addsproplem2  27978  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  negsid  28049  mulsproplem9  28132  sltmuls1  28155  sltmuls2  28156  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  precsexlem9  28223  precsexlem11  28225  clwwlkneq0  30116  ofpreima2  32756  odutos  33061  trleile  33064  domnprodeq0  33370  prmidl2  33534  prmidl0  33543  smatrcl  33974  ordtconnlem1  34102  sitgaddlemb  34526  satfvsuclem2  35576  satfvsucsuc  35581  satfdm  35585  satf0  35588  satffunlem2lem1  35620  dmopab3rexdif  35621  quad3  35886  nepss  35934  dfso2  35971  dfon2lem4  36000  dfon2lem5  36001  dfon3  36106  brcup  36153  dfrdg4  36167  hfun  36394  sumeq2si  36418  prodeq2si  36420  cbvprodvw2  36463  bj-df-ifc  36805  bj-eltag  37225  bj-projun  37242  poimirlem22  37893  poimirlem31  37902  poimirlem32  37903  ispridl2  38289  smprngopr  38303  isdmn3  38325  sbcori  38360  tsbi4  38387  dfsucmap3  38714  4atlem3  39972  elpadd  40175  paddasslem17  40212  cdlemg31b0N  41070  cdlemg31b0a  41071  cdlemh  41193  jm2.23  43353  ifpim123g  43856  ifpananb  43862  rp-isfinite6  43874  iunrelexp0  44058  clsk1indlem3  44399  permaxinf2lem  45368  aovov0bi  47556  zeoALTV  48030  divgcdoddALTV  48042  clnbgrsym  48198  dfclnbgr6  48216  usgrexmpl2nb0  48391  usgrexmpl2nb1  48392  usgrexmpl2nb2  48393  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  usgrexmpl2trifr  48397  rrx2pnedifcoorneor  49076  line2xlem  49113