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  2334  neorian  3023  sspsstri  4052  rexun  4143  elsymdif  4205  indi  4231  unabw  4254  unab  4255  dfnf5  4329  ab0orv  4330  inundif  4426  dfpr2  4594  ssunsn  4777  ssunpr  4783  sspr  4784  sstp  4785  prneimg  4803  prneimg2  4804  prnebg  4805  pwpr  4850  pwtp  4851  uniun  4879  iunun  5039  iunxun  5040  brun  5140  zfpair  5357  opthneg  5419  propeqop  5445  opthprc  5678  dmopab2rex  5856  xpeq0  6107  difxp  6111  ordtri2or3  6408  ftpg  7089  ordunpr  7756  xpord2pred  8075  xpord3pred  8082  mpoxneldm  8142  tpostpos  8176  frrlem13  8228  oarec  8477  brdom2  8904  modom  9135  dfsup2  9328  wemapsolem  9436  djuunxp  9814  leweon  9902  kmlem16  10057  fin23lem40  10242  axpre-lttri  11056  nn0n0n1ge2b  12450  elnn0z  12481  fz0  13439  sqeqori  14121  hashtpg  14392  swrdnnn0nd  14564  swrdnd0  14565  cbvsum  15602  cbvsumv  15603  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  rpnnen2lem12  16134  lcmfpr  16538  pythagtriplem2  16729  pythagtrip  16746  mreexexd  17554  smndex1basss  18813  smndex1mgm  18815  smndex1n0mnd  18820  opprdomnb  20632  cnfldfun  21305  cnfldfunOLD  21318  ppttop  22922  fixufil  23837  alexsubALTlem2  23963  alexsubALTlem3  23964  alexsubALTlem4  23965  dyaddisj  25524  noetalem1  27680  addsproplem2  27913  sleadd1  27932  addsuniflem  27944  addsasslem1  27946  addsasslem2  27947  negsid  27983  mulsproplem9  28063  ssltmul1  28086  ssltmul2  28087  addsdilem1  28090  addsdilem2  28091  mulsasslem1  28102  mulsasslem2  28103  precsexlem9  28153  precsexlem11  28155  clwwlkneq0  30009  ofpreima2  32648  odutos  32949  trleile  32952  prmidl2  33406  prmidl0  33415  smatrcl  33809  ordtconnlem1  33937  sitgaddlemb  34361  satfvsuclem2  35404  satfvsucsuc  35409  satfdm  35413  satf0  35416  satffunlem2lem1  35448  dmopab3rexdif  35449  quad3  35714  nepss  35762  dfso2  35799  dfon2lem4  35828  dfon2lem5  35829  dfon3  35934  brcup  35981  dfrdg4  35995  hfun  36222  sumeq2si  36246  prodeq2si  36248  cbvprodvw2  36291  bj-df-ifc  36624  bj-eltag  37021  bj-projun  37038  poimirlem22  37692  poimirlem31  37701  poimirlem32  37702  ispridl2  38088  smprngopr  38102  isdmn3  38124  sbcori  38159  tsbi4  38186  dfsucmap3  38486  4atlem3  39705  elpadd  39908  paddasslem17  39945  cdlemg31b0N  40803  cdlemg31b0a  40804  cdlemh  40926  jm2.23  43099  ifpim123g  43603  ifpananb  43609  rp-isfinite6  43621  iunrelexp0  43805  clsk1indlem3  44146  permaxinf2lem  45115  aovov0bi  47306  zeoALTV  47780  divgcdoddALTV  47792  clnbgrsym  47948  dfclnbgr6  47966  usgrexmpl2nb0  48141  usgrexmpl2nb1  48142  usgrexmpl2nb2  48143  usgrexmpl2nb3  48144  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  usgrexmpl2trifr  48147  rrx2pnedifcoorneor  48827  line2xlem  48864