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  2338  neorian  3027  sspsstri  4057  rexun  4148  elsymdif  4210  indi  4236  unabw  4259  unab  4260  dfnf5  4334  ab0orv  4335  inundif  4431  dfpr2  4601  ssunsn  4784  ssunpr  4790  sspr  4791  sstp  4792  prneimg  4810  prneimg2  4811  prnebg  4812  pwpr  4857  pwtp  4858  uniun  4886  iunun  5048  iunxun  5049  brun  5149  zfpair  5366  opthneg  5429  propeqop  5455  opthprc  5688  dmopab2rex  5866  xpeq0  6118  difxp  6122  ordtri2or3  6419  ftpg  7101  ordunpr  7768  xpord2pred  8087  xpord3pred  8094  mpoxneldm  8154  tpostpos  8188  frrlem13  8240  oarec  8489  brdom2  8919  modom  9151  dfsup2  9347  wemapsolem  9455  djuunxp  9833  leweon  9921  kmlem16  10076  fin23lem40  10261  axpre-lttri  11076  nn0n0n1ge2b  12470  elnn0z  12501  fz0  13455  sqeqori  14137  hashtpg  14408  swrdnnn0nd  14580  swrdnd0  14581  cbvsum  15618  cbvsumv  15619  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  rpnnen2lem12  16150  lcmfpr  16554  pythagtriplem2  16745  pythagtrip  16762  mreexexd  17571  smndex1basss  18830  smndex1mgm  18832  smndex1n0mnd  18837  opprdomnb  20650  cnfldfun  21323  cnfldfunOLD  21336  ppttop  22951  fixufil  23866  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  dyaddisj  25553  noetalem1  27709  addsproplem2  27966  leadds1  27985  addsuniflem  27997  addsasslem1  27999  addsasslem2  28000  negsid  28037  mulsproplem9  28120  sltmuls1  28143  sltmuls2  28144  addsdilem1  28147  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  precsexlem9  28211  precsexlem11  28213  clwwlkneq0  30104  ofpreima2  32744  odutos  33050  trleile  33053  domnprodeq0  33358  prmidl2  33522  prmidl0  33531  smatrcl  33953  ordtconnlem1  34081  sitgaddlemb  34505  satfvsuclem2  35554  satfvsucsuc  35559  satfdm  35563  satf0  35566  satffunlem2lem1  35598  dmopab3rexdif  35599  quad3  35864  nepss  35912  dfso2  35949  dfon2lem4  35978  dfon2lem5  35979  dfon3  36084  brcup  36131  dfrdg4  36145  hfun  36372  sumeq2si  36396  prodeq2si  36398  cbvprodvw2  36441  bj-df-ifc  36780  bj-eltag  37178  bj-projun  37195  poimirlem22  37843  poimirlem31  37852  poimirlem32  37853  ispridl2  38239  smprngopr  38253  isdmn3  38275  sbcori  38310  tsbi4  38337  dfsucmap3  38637  4atlem3  39856  elpadd  40059  paddasslem17  40096  cdlemg31b0N  40954  cdlemg31b0a  40955  cdlemh  41077  jm2.23  43238  ifpim123g  43741  ifpananb  43747  rp-isfinite6  43759  iunrelexp0  43943  clsk1indlem3  44284  permaxinf2lem  45253  aovov0bi  47442  zeoALTV  47916  divgcdoddALTV  47928  clnbgrsym  48084  dfclnbgr6  48102  usgrexmpl2nb0  48277  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  rrx2pnedifcoorneor  48962  line2xlem  48999