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  4068  rexun  4159  elsymdif  4221  indi  4247  unabw  4270  unab  4271  dfnf5  4345  ab0orv  4346  inundif  4442  dfpr2  4610  ssunsn  4792  ssunpr  4798  sspr  4799  sstp  4800  prneimg  4818  prneimg2  4819  prnebg  4820  pwpr  4865  pwtp  4866  uniun  4894  iunun  5057  iunxun  5058  brun  5158  zfpair  5376  opthneg  5441  propeqop  5467  opthprc  5702  dmopab2rex  5881  xpeq0  6133  difxp  6137  ordtri2or3  6434  ftpg  7128  ordunpr  7801  xpord2pred  8124  xpord3pred  8131  mpoxneldm  8191  tpostpos  8225  frrlem13  8277  oarec  8526  brdom2  8953  modom  9191  dfsup2  9395  wemapsolem  9503  djuunxp  9874  leweon  9964  kmlem16  10119  fin23lem40  10304  axpre-lttri  11118  nn0n0n1ge2b  12511  elnn0z  12542  fz0  13500  sqeqori  14179  hashtpg  14450  swrdnnn0nd  14621  swrdnd0  14622  cbvsum  15661  cbvsumv  15662  cbvprod  15879  cbvprodv  15880  prodeq1i  15882  rpnnen2lem12  16193  lcmfpr  16597  pythagtriplem2  16788  pythagtrip  16805  mreexexd  17609  smndex1basss  18832  smndex1mgm  18834  smndex1n0mnd  18839  opprdomnb  20626  cnfldfun  21278  cnfldfunOLD  21291  ppttop  22894  fixufil  23809  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  dyaddisj  25497  noetalem1  27653  addsproplem2  27877  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  negsid  27947  mulsproplem9  28027  ssltmul1  28050  ssltmul2  28051  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  precsexlem9  28117  precsexlem11  28119  clwwlkneq0  29958  ofpreima2  32590  odutos  32894  trleile  32897  prmidl2  33412  prmidl0  33421  smatrcl  33786  ordtconnlem1  33914  sitgaddlemb  34339  satfvsuclem2  35347  satfvsucsuc  35352  satfdm  35356  satf0  35359  satffunlem2lem1  35391  dmopab3rexdif  35392  quad3  35657  nepss  35705  dfso2  35742  dfon2lem4  35774  dfon2lem5  35775  dfon3  35880  brcup  35927  dfrdg4  35939  hfun  36166  sumeq2si  36190  prodeq2si  36192  cbvprodvw2  36235  bj-df-ifc  36568  bj-eltag  36965  bj-projun  36982  poimirlem22  37636  poimirlem31  37645  poimirlem32  37646  ispridl2  38032  smprngopr  38046  isdmn3  38068  sbcori  38103  tsbi4  38130  4atlem3  39590  elpadd  39793  paddasslem17  39830  cdlemg31b0N  40688  cdlemg31b0a  40689  cdlemh  40811  jm2.23  42985  ifpim123g  43489  ifpananb  43495  rp-isfinite6  43507  iunrelexp0  43691  clsk1indlem3  44032  permaxinf2lem  45002  aovov0bi  47197  zeoALTV  47671  divgcdoddALTV  47683  clnbgrsym  47838  dfclnbgr6  47856  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  rrx2pnedifcoorneor  48705  line2xlem  48742