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  4064  rexun  4155  elsymdif  4217  indi  4243  unabw  4266  unab  4267  dfnf5  4341  ab0orv  4342  inundif  4438  dfpr2  4606  ssunsn  4788  ssunpr  4794  sspr  4795  sstp  4796  prneimg  4814  prneimg2  4815  prnebg  4816  pwpr  4861  pwtp  4862  uniun  4890  iunun  5052  iunxun  5053  brun  5153  zfpair  5371  opthneg  5436  propeqop  5462  opthprc  5695  dmopab2rex  5871  xpeq0  6121  difxp  6125  ordtri2or3  6422  ftpg  7110  ordunpr  7781  xpord2pred  8101  xpord3pred  8108  mpoxneldm  8168  tpostpos  8202  frrlem13  8254  oarec  8503  brdom2  8930  modom  9167  dfsup2  9371  wemapsolem  9479  djuunxp  9850  leweon  9940  kmlem16  10095  fin23lem40  10280  axpre-lttri  11094  nn0n0n1ge2b  12487  elnn0z  12518  fz0  13476  sqeqori  14155  hashtpg  14426  swrdnnn0nd  14597  swrdnd0  14598  cbvsum  15637  cbvsumv  15638  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  rpnnen2lem12  16169  lcmfpr  16573  pythagtriplem2  16764  pythagtrip  16781  mreexexd  17585  smndex1basss  18808  smndex1mgm  18810  smndex1n0mnd  18815  opprdomnb  20602  cnfldfun  21254  cnfldfunOLD  21267  ppttop  22870  fixufil  23785  alexsubALTlem2  23911  alexsubALTlem3  23912  alexsubALTlem4  23913  dyaddisj  25473  noetalem1  27629  addsproplem2  27853  sleadd1  27872  addsuniflem  27884  addsasslem1  27886  addsasslem2  27887  negsid  27923  mulsproplem9  28003  ssltmul1  28026  ssltmul2  28027  addsdilem1  28030  addsdilem2  28031  mulsasslem1  28042  mulsasslem2  28043  precsexlem9  28093  precsexlem11  28095  clwwlkneq0  29931  ofpreima2  32563  odutos  32867  trleile  32870  prmidl2  33385  prmidl0  33394  smatrcl  33759  ordtconnlem1  33887  sitgaddlemb  34312  satfvsuclem2  35320  satfvsucsuc  35325  satfdm  35329  satf0  35332  satffunlem2lem1  35364  dmopab3rexdif  35365  quad3  35630  nepss  35678  dfso2  35715  dfon2lem4  35747  dfon2lem5  35748  dfon3  35853  brcup  35900  dfrdg4  35912  hfun  36139  sumeq2si  36163  prodeq2si  36165  cbvprodvw2  36208  bj-df-ifc  36541  bj-eltag  36938  bj-projun  36955  poimirlem22  37609  poimirlem31  37618  poimirlem32  37619  ispridl2  38005  smprngopr  38019  isdmn3  38041  sbcori  38076  tsbi4  38103  4atlem3  39563  elpadd  39766  paddasslem17  39803  cdlemg31b0N  40661  cdlemg31b0a  40662  cdlemh  40784  jm2.23  42958  ifpim123g  43462  ifpananb  43468  rp-isfinite6  43480  iunrelexp0  43664  clsk1indlem3  44005  permaxinf2lem  44975  aovov0bi  47170  zeoALTV  47644  divgcdoddALTV  47656  clnbgrsym  47811  dfclnbgr6  47829  usgrexmpl2nb0  47995  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  rrx2pnedifcoorneor  48678  line2xlem  48715