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  1155  3or6  1446  noran  1528  cadcoma  1608  eeor  2333  neorian  3034  sspsstri  4114  rexun  4205  elsymdif  4263  indi  4289  unabw  4312  unab  4313  dfnf5  4387  ab0orv  4388  inundif  4484  dfpr2  4650  ssunsn  4832  ssunpr  4838  sspr  4839  sstp  4840  prneimg  4858  prneimg2  4859  prnebg  4860  pwpr  4905  pwtp  4906  uniun  4934  iunun  5097  iunxun  5098  brun  5198  zfpair  5426  opthneg  5491  propeqop  5516  opthprc  5752  dmopab2rex  5930  xpeq0  6181  difxp  6185  ordtri2or3  6485  ftpg  7175  ordunpr  7845  xpord2pred  8168  xpord3pred  8175  mpoxneldm  8235  tpostpos  8269  frrlem13  8321  oarec  8598  brdom2  9020  modom  9277  dfsup2  9481  wemapsolem  9587  djuunxp  9958  leweon  10048  kmlem16  10203  fin23lem40  10388  axpre-lttri  11202  nn0n0n1ge2b  12592  elnn0z  12623  fz0  13575  sqeqori  14249  hashtpg  14520  swrdnnn0nd  14690  swrdnd0  14691  cbvsum  15727  cbvsumv  15728  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  rpnnen2lem12  16257  lcmfpr  16660  pythagtriplem2  16850  pythagtrip  16867  mreexexd  17692  smndex1basss  18930  smndex1mgm  18932  smndex1n0mnd  18937  opprdomnb  20733  cnfldfun  21395  cnfldfunOLD  21408  ppttop  23029  fixufil  23945  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  dyaddisj  25644  noetalem1  27800  addsproplem2  28017  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  negsid  28087  mulsproplem9  28164  ssltmul1  28187  ssltmul2  28188  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  precsexlem9  28253  precsexlem11  28255  clwwlkneq0  30057  ofpreima2  32682  odutos  32942  trleile  32945  prmidl2  33448  prmidl0  33457  smatrcl  33756  ordtconnlem1  33884  sitgaddlemb  34329  satfvsuclem2  35344  satfvsucsuc  35349  satfdm  35353  satf0  35356  satffunlem2lem1  35388  dmopab3rexdif  35389  quad3  35654  nepss  35697  dfso2  35734  dfon2lem4  35767  dfon2lem5  35768  dfon3  35873  brcup  35920  dfrdg4  35932  hfun  36159  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36229  bj-df-ifc  36562  bj-eltag  36959  bj-projun  36976  poimirlem22  37628  poimirlem31  37637  poimirlem32  37638  ispridl2  38024  smprngopr  38038  isdmn3  38060  sbcori  38095  tsbi4  38122  4atlem3  39578  elpadd  39781  paddasslem17  39818  cdlemg31b0N  40676  cdlemg31b0a  40677  cdlemh  40799  jm2.23  42984  ifpim123g  43489  ifpananb  43495  rp-isfinite6  43507  iunrelexp0  43691  clsk1indlem3  44032  aovov0bi  47145  zeoALTV  47594  divgcdoddALTV  47606  clnbgrsym  47761  dfclnbgr6  47779  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  rrx2pnedifcoorneor  48565  line2xlem  48602