Theorem orbi12i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 846

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 847

This theorem is referenced by:  pm4.78  933  andir  1009  anddi  1011  cases  1043  cases2  1048  3orbi123i  1156  3or6  1447  noran  1529  cadcoma  1609  eeor  2339  neorian  3043  sspsstri  4128  rexun  4219  elsymdif  4277  indi  4303  unabw  4326  unab  4327  dfnf5  4405  ab0orv  4406  inundif  4502  dfpr2  4668  ssunsn  4853  ssunpr  4859  sspr  4860  sstp  4861  prneimg  4879  prnebg  4880  pwpr  4925  pwtp  4926  uniun  4954  iunun  5116  iunxun  5117  brun  5217  zfpair  5439  opthneg  5501  propeqop  5526  opthprc  5764  dmopab2rex  5942  xpeq0  6191  difxp  6195  ordtri2or3  6495  ftpg  7190  ordunpr  7862  xpord2pred  8186  xpord3pred  8193  mpoxneldm  8253  tpostpos  8287  frrlem13  8339  oarec  8618  brdom2  9042  modom  9307  dfsup2  9513  wemapsolem  9619  djuunxp  9990  leweon  10080  kmlem16  10235  fin23lem40  10420  axpre-lttri  11234  nn0n0n1ge2b  12621  elnn0z  12652  fz0  13599  sqeqori  14263  hashtpg  14534  swrdnnn0nd  14704  swrdnd0  14705  cbvsum  15743  cbvsumv  15744  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  rpnnen2lem12  16273  lcmfpr  16674  pythagtriplem2  16864  pythagtrip  16881  mreexexd  17706  smndex1basss  18940  smndex1mgm  18942  smndex1n0mnd  18947  opprdomnb  20739  cnfldfun  21401  cnfldfunOLD  21414  ppttop  23035  fixufil  23951  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  dyaddisj  25650  noetalem1  27804  addsproplem2  28021  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  negsid  28091  mulsproplem9  28168  ssltmul1  28191  ssltmul2  28192  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  precsexlem9  28257  precsexlem11  28259  clwwlkneq0  30061  ofpreima2  32684  odutos  32941  trleile  32944  prmidl2  33434  prmidl0  33443  smatrcl  33742  ordtconnlem1  33870  sitgaddlemb  34313  satfvsuclem2  35328  satfvsucsuc  35333  satfdm  35337  satf0  35340  satffunlem2lem1  35372  dmopab3rexdif  35373  quad3  35638  nepss  35680  dfso2  35717  dfon2lem4  35750  dfon2lem5  35751  dfon3  35856  brcup  35903  dfrdg4  35915  hfun  36142  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36213  bj-df-ifc  36546  bj-eltag  36943  bj-projun  36960  poimirlem22  37602  poimirlem31  37611  poimirlem32  37612  ispridl2  37998  smprngopr  38012  isdmn3  38034  sbcori  38069  tsbi4  38096  4atlem3  39553  elpadd  39756  paddasslem17  39793  cdlemg31b0N  40651  cdlemg31b0a  40652  cdlemh  40774  jm2.23  42953  ifpim123g  43462  ifpananb  43468  rp-isfinite6  43480  iunrelexp0  43664  clsk1indlem3  44005  aovov0bi  47111  zeoALTV  47544  divgcdoddALTV  47556  clnbgrsym  47710  dfclnbgr6  47728  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  rrx2pnedifcoorneor  48450  line2xlem  48487