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  1533  cadcoma  1613  eeor  2336  neorian  3025  sspsstri  4055  rexun  4146  elsymdif  4208  indi  4234  unabw  4257  unab  4258  dfnf5  4332  ab0orv  4333  inundif  4429  dfpr2  4599  ssunsn  4782  ssunpr  4788  sspr  4789  sstp  4790  prneimg  4808  prneimg2  4809  prnebg  4810  pwpr  4855  pwtp  4856  uniun  4884  iunun  5046  iunxun  5047  brun  5147  zfpair  5364  opthneg  5427  propeqop  5453  opthprc  5686  dmopab2rex  5864  xpeq0  6116  difxp  6120  ordtri2or3  6417  ftpg  7099  ordunpr  7766  xpord2pred  8085  xpord3pred  8092  mpoxneldm  8152  tpostpos  8186  frrlem13  8238  oarec  8487  brdom2  8917  modom  9149  dfsup2  9345  wemapsolem  9453  djuunxp  9831  leweon  9919  kmlem16  10074  fin23lem40  10259  axpre-lttri  11074  nn0n0n1ge2b  12468  elnn0z  12499  fz0  13453  sqeqori  14135  hashtpg  14406  swrdnnn0nd  14578  swrdnd0  14579  cbvsum  15616  cbvsumv  15617  cbvprod  15834  cbvprodv  15835  prodeq1i  15837  rpnnen2lem12  16148  lcmfpr  16552  pythagtriplem2  16743  pythagtrip  16760  mreexexd  17569  smndex1basss  18828  smndex1mgm  18830  smndex1n0mnd  18835  opprdomnb  20648  cnfldfun  21321  cnfldfunOLD  21334  ppttop  22949  fixufil  23864  alexsubALTlem2  23990  alexsubALTlem3  23991  alexsubALTlem4  23992  dyaddisj  25551  noetalem1  27707  addsproplem2  27940  sleadd1  27959  addsuniflem  27971  addsasslem1  27973  addsasslem2  27974  negsid  28010  mulsproplem9  28093  ssltmul1  28116  ssltmul2  28117  addsdilem1  28120  addsdilem2  28121  mulsasslem1  28132  mulsasslem2  28133  precsexlem9  28183  precsexlem11  28185  clwwlkneq0  30053  ofpreima2  32693  odutos  32999  trleile  33002  domnprodeq0  33307  prmidl2  33471  prmidl0  33480  smatrcl  33902  ordtconnlem1  34030  sitgaddlemb  34454  satfvsuclem2  35503  satfvsucsuc  35508  satfdm  35512  satf0  35515  satffunlem2lem1  35547  dmopab3rexdif  35548  quad3  35813  nepss  35861  dfso2  35898  dfon2lem4  35927  dfon2lem5  35928  dfon3  36033  brcup  36080  dfrdg4  36094  hfun  36321  sumeq2si  36345  prodeq2si  36347  cbvprodvw2  36390  bj-df-ifc  36723  bj-eltag  37121  bj-projun  37138  poimirlem22  37782  poimirlem31  37791  poimirlem32  37792  ispridl2  38178  smprngopr  38192  isdmn3  38214  sbcori  38249  tsbi4  38276  dfsucmap3  38576  4atlem3  39795  elpadd  39998  paddasslem17  40035  cdlemg31b0N  40893  cdlemg31b0a  40894  cdlemh  41016  jm2.23  43180  ifpim123g  43683  ifpananb  43689  rp-isfinite6  43701  iunrelexp0  43885  clsk1indlem3  44226  permaxinf2lem  45195  aovov0bi  47384  zeoALTV  47858  divgcdoddALTV  47870  clnbgrsym  48026  dfclnbgr6  48044  usgrexmpl2nb0  48219  usgrexmpl2nb1  48220  usgrexmpl2nb2  48221  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225  rrx2pnedifcoorneor  48904  line2xlem  48941