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  17589  smndex1basss  18814  smndex1mgm  18816  smndex1n0mnd  18821  opprdomnb  20637  cnfldfun  21310  cnfldfunOLD  21323  ppttop  22927  fixufil  23842  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  dyaddisj  25530  noetalem1  27686  addsproplem2  27917  sleadd1  27936  addsuniflem  27948  addsasslem1  27950  addsasslem2  27951  negsid  27987  mulsproplem9  28067  ssltmul1  28090  ssltmul2  28091  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  precsexlem9  28157  precsexlem11  28159  clwwlkneq0  30008  ofpreima2  32640  odutos  32940  trleile  32943  prmidl2  33405  prmidl0  33414  smatrcl  33779  ordtconnlem1  33907  sitgaddlemb  34332  satfvsuclem2  35340  satfvsucsuc  35345  satfdm  35349  satf0  35352  satffunlem2lem1  35384  dmopab3rexdif  35385  quad3  35650  nepss  35698  dfso2  35735  dfon2lem4  35767  dfon2lem5  35768  dfon3  35873  brcup  35920  dfrdg4  35932  hfun  36159  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36228  bj-df-ifc  36561  bj-eltag  36958  bj-projun  36975  poimirlem22  37629  poimirlem31  37638  poimirlem32  37639  ispridl2  38025  smprngopr  38039  isdmn3  38061  sbcori  38096  tsbi4  38123  4atlem3  39583  elpadd  39786  paddasslem17  39823  cdlemg31b0N  40681  cdlemg31b0a  40682  cdlemh  40804  jm2.23  42978  ifpim123g  43482  ifpananb  43488  rp-isfinite6  43500  iunrelexp0  43684  clsk1indlem3  44025  permaxinf2lem  44995  aovov0bi  47190  zeoALTV  47664  divgcdoddALTV  47676  clnbgrsym  47831  dfclnbgr6  47849  usgrexmpl2nb0  48015  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  rrx2pnedifcoorneor  48698  line2xlem  48735