Theorem orbi12i 915

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 913	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 914	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 275	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  pm4.78  935  andir  1011  anddi  1013  cases  1043  cases2  1048  3orbi123i  1157  3or6  1449  noran  1532  cadcoma  1612  eeor  2335  neorian  3037  sspsstri  4105  rexun  4196  elsymdif  4258  indi  4284  unabw  4307  unab  4308  dfnf5  4382  ab0orv  4383  inundif  4479  dfpr2  4646  ssunsn  4828  ssunpr  4834  sspr  4835  sstp  4836  prneimg  4854  prneimg2  4855  prnebg  4856  pwpr  4901  pwtp  4902  uniun  4930  iunun  5093  iunxun  5094  brun  5194  zfpair  5421  opthneg  5486  propeqop  5512  opthprc  5749  dmopab2rex  5928  xpeq0  6180  difxp  6184  ordtri2or3  6484  ftpg  7176  ordunpr  7846  xpord2pred  8170  xpord3pred  8177  mpoxneldm  8237  tpostpos  8271  frrlem13  8323  oarec  8600  brdom2  9022  modom  9280  dfsup2  9484  wemapsolem  9590  djuunxp  9961  leweon  10051  kmlem16  10206  fin23lem40  10391  axpre-lttri  11205  nn0n0n1ge2b  12595  elnn0z  12626  fz0  13579  sqeqori  14253  hashtpg  14524  swrdnnn0nd  14694  swrdnd0  14695  cbvsum  15731  cbvsumv  15732  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  rpnnen2lem12  16261  lcmfpr  16664  pythagtriplem2  16855  pythagtrip  16872  mreexexd  17691  smndex1basss  18918  smndex1mgm  18920  smndex1n0mnd  18925  opprdomnb  20717  cnfldfun  21378  cnfldfunOLD  21391  ppttop  23014  fixufil  23930  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  dyaddisj  25631  noetalem1  27786  addsproplem2  28003  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  negsid  28073  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  precsexlem9  28239  precsexlem11  28241  clwwlkneq0  30048  ofpreima2  32676  odutos  32958  trleile  32961  prmidl2  33469  prmidl0  33478  smatrcl  33795  ordtconnlem1  33923  sitgaddlemb  34350  satfvsuclem2  35365  satfvsucsuc  35370  satfdm  35374  satf0  35377  satffunlem2lem1  35409  dmopab3rexdif  35410  quad3  35675  nepss  35718  dfso2  35755  dfon2lem4  35787  dfon2lem5  35788  dfon3  35893  brcup  35940  dfrdg4  35952  hfun  36179  sumeq2si  36203  prodeq2si  36205  cbvprodvw2  36248  bj-df-ifc  36581  bj-eltag  36978  bj-projun  36995  poimirlem22  37649  poimirlem31  37658  poimirlem32  37659  ispridl2  38045  smprngopr  38059  isdmn3  38081  sbcori  38116  tsbi4  38143  4atlem3  39598  elpadd  39801  paddasslem17  39838  cdlemg31b0N  40696  cdlemg31b0a  40697  cdlemh  40819  jm2.23  43008  ifpim123g  43513  ifpananb  43519  rp-isfinite6  43531  iunrelexp0  43715  clsk1indlem3  44056  aovov0bi  47208  zeoALTV  47657  divgcdoddALTV  47669  clnbgrsym  47824  dfclnbgr6  47842  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  rrx2pnedifcoorneor  48637  line2xlem  48674