Theorem orbi12i 928

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.78  948  andir  1026  anddi  1028  cases  1058  cases2  1063  3orbi123i  1174  3or6  1476  noran  1562  cadcoma  1645  eeor  2364  neorian  3051  sspsstri  4054  rexun  4142  elsymdif  4204  indi  4230  unabw  4253  unab  4254  dfnf5  4331  ab0orv  4332  inundif  4435  dfpr2  4605  ssunsn  4789  ssunpr  4794  sspr  4795  sstp  4796  prneimg  4814  prneimg2  4815  prnebg  4816  pwpr  4861  pwtp  4862  uniun  4890  iunun  5053  iunxun  5054  brun  5156  zfpair  5383  opthneg  5450  propeqop  5479  opthprc  5715  dmopab2rex  5899  xpeq0  6151  difxp  6155  ordtri2or3  6465  ftpg  7160  ordunpr  7837  xpord2pred  8162  xpord3pred  8169  mpoxneldm  8229  tpostpos  8263  frrlem13  8316  oarec  8570  brdom2  9009  modom  9242  dfsup2  9436  wemapsolem  9544  hfunOLD  9919  djuunxp  10002  leweon  10090  kmlem16  10244  fin23lem40  10429  axpre-lttri  11250  nn0n0n1ge2b  12675  elnn0z  12706  fz0  13672  sqeqori  14358  hashtpg  14630  swrdnnn0nd  14806  swrdnd0  14807  cbvsum  15862  cbvsumv  15863  cbvprod  16082  cbvprodv  16083  prodeq1i  16085  rpnnen2lem12  16393  lcmfpr  16802  pythagtriplem2  16995  pythagtrip  17012  mreexexd  17822  smndex1basss  19104  smndex1mgm  19106  smndex1n0mnd  19111  opprdomnb  20968  prmidl2  21622  prmidl0  21634  cnfldfun  21692  ppttop  23325  fixufil  24241  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  dyaddisj  25917  noetalem1  28098  addsproplem2  28356  leadds1  28375  addsuniflem  28387  addsasslem1  28389  addsasslem2  28390  negsid  28427  mulsproplem9  28510  sltmuls1  28533  sltmuls2  28534  addsdilem1  28537  addsdilem2  28538  mulsasslem1  28549  mulsasslem2  28550  precsexlem9  28601  precsexlem11  28603  clwwlkneq0  30620  ofpreima2  33260  odutos  33529  trleile  33532  domnprodeq0  33840  smatrcl  34428  ordtconnlem1  34556  sitgaddlemb  34980  satfvsuclem2  36125  satfvsucsuc  36130  satfdm  36134  satf0  36137  satffunlem2lem1  36169  dmopab3rexdif  36170  quad3  36435  nepss  36483  dfso2  36520  dfon2lem4  36548  dfon2lem5  36549  dfon3  36654  brcup  36701  dfrdg4  36715  ltnadd  36967  naddle  36968  sumeq2si  36991  prodeq2si  36993  cbvprodvw2  37036  bj-df-ifc  37450  bj-eltag  37890  bj-projun  37907  poimirlem22  38560  poimirlem31  38569  poimirlem32  38570  ispridl2  38972  smprngopr  38986  isdmn3  39008  sbcori  39041  tsbi4  39068  dfsucmap3  39395  4atlem3  40653  elpadd  40856  paddasslem17  40893  cdlemg31b0N  41751  cdlemg31b0a  41752  cdlemh  41874  jm2.23  44002  ifpim123g  44500  ifpananb  44506  rp-isfinite6  44518  iunrelexp0  44701  clsk1indlem3  45042  permaxinf2lem  46001  aovov0bi  48265  zeoALTV  48767  divgcdoddALTV  48779  clnbgrsym  48935  dfclnbgr6  48953  usgrexmpl2nb0  49128  usgrexmpl2nb1  49129  usgrexmpl2nb2  49130  usgrexmpl2nb3  49131  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  smprngprmrng  49435  isidom3  49441  rrx2pnedifcoorneor  49827  line2xlem  49864