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  4056  rexun  4147  elsymdif  4209  indi  4235  unabw  4258  unab  4259  dfnf5  4333  ab0orv  4334  inundif  4430  dfpr2  4598  ssunsn  4779  ssunpr  4785  sspr  4786  sstp  4787  prneimg  4805  prneimg2  4806  prnebg  4807  pwpr  4852  pwtp  4853  uniun  4881  iunun  5042  iunxun  5043  brun  5143  zfpair  5360  opthneg  5424  propeqop  5450  opthprc  5683  dmopab2rex  5860  xpeq0  6109  difxp  6113  ordtri2or3  6409  ftpg  7090  ordunpr  7759  xpord2pred  8078  xpord3pred  8085  mpoxneldm  8145  tpostpos  8179  frrlem13  8231  oarec  8480  brdom2  8907  modom  9140  dfsup2  9334  wemapsolem  9442  djuunxp  9817  leweon  9905  kmlem16  10060  fin23lem40  10245  axpre-lttri  11059  nn0n0n1ge2b  12453  elnn0z  12484  fz0  13442  sqeqori  14121  hashtpg  14392  swrdnnn0nd  14563  swrdnd0  14564  cbvsum  15602  cbvsumv  15603  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  rpnnen2lem12  16134  lcmfpr  16538  pythagtriplem2  16729  pythagtrip  16746  mreexexd  17554  smndex1basss  18779  smndex1mgm  18781  smndex1n0mnd  18786  opprdomnb  20602  cnfldfun  21275  cnfldfunOLD  21288  ppttop  22892  fixufil  23807  alexsubALTlem2  23933  alexsubALTlem3  23934  alexsubALTlem4  23935  dyaddisj  25495  noetalem1  27651  addsproplem2  27882  sleadd1  27901  addsuniflem  27913  addsasslem1  27915  addsasslem2  27916  negsid  27952  mulsproplem9  28032  ssltmul1  28055  ssltmul2  28056  addsdilem1  28059  addsdilem2  28060  mulsasslem1  28071  mulsasslem2  28072  precsexlem9  28122  precsexlem11  28124  clwwlkneq0  29973  ofpreima2  32609  odutos  32910  trleile  32913  prmidl2  33378  prmidl0  33387  smatrcl  33763  ordtconnlem1  33891  sitgaddlemb  34316  satfvsuclem2  35337  satfvsucsuc  35342  satfdm  35346  satf0  35349  satffunlem2lem1  35381  dmopab3rexdif  35382  quad3  35647  nepss  35695  dfso2  35732  dfon2lem4  35764  dfon2lem5  35765  dfon3  35870  brcup  35917  dfrdg4  35929  hfun  36156  sumeq2si  36180  prodeq2si  36182  cbvprodvw2  36225  bj-df-ifc  36558  bj-eltag  36955  bj-projun  36972  poimirlem22  37626  poimirlem31  37635  poimirlem32  37636  ispridl2  38022  smprngopr  38036  isdmn3  38058  sbcori  38093  tsbi4  38120  4atlem3  39579  elpadd  39782  paddasslem17  39819  cdlemg31b0N  40677  cdlemg31b0a  40678  cdlemh  40800  jm2.23  42973  ifpim123g  43477  ifpananb  43483  rp-isfinite6  43495  iunrelexp0  43679  clsk1indlem3  44020  permaxinf2lem  44990  aovov0bi  47184  zeoALTV  47658  divgcdoddALTV  47670  clnbgrsym  47826  dfclnbgr6  47844  usgrexmpl2nb0  48019  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  usgrexmpl2nb3  48022  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  usgrexmpl2trifr  48025  rrx2pnedifcoorneor  48705  line2xlem  48742