Theorem orbi12i 912

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

Syntax hints:   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  pm4.78  932  andir  1006  anddi  1008  cases  1038  cases2  1043  3orbi123i  1153  3or6  1444  noran  1527  noranOLD  1528  cadcoma  1614  neorian  3081  sspsstri  4030  rexun  4117  elsymdif  4174  indi  4200  unab  4222  dfnf5  4288  inundif  4385  dfpr2  4544  ssunsn  4721  ssunpr  4725  sspr  4726  sstp  4727  prneimg  4745  prnebg  4746  pwpr  4794  pwtp  4795  unipr  4817  uniun  4823  iunun  4978  iunxun  4979  brun  5081  zfpair  5287  opthneg  5338  propeqop  5362  pwunssOLD  5420  opthprc  5580  dmopab2rex  5750  xpeq0  5984  difxp  5988  ordtri2or3  6256  ftpg  6895  ordunpr  7521  mpoxneldm  7861  tpostpos  7895  oarec  8171  brdom2  8522  modom  8703  dfsup2  8892  wemapsolem  8998  djuunxp  9334  leweon  9422  kmlem16  9576  fin23lem40  9762  axpre-lttri  10576  nn0n0n1ge2b  11951  elnn0z  11982  fz0  12917  sqeqori  13572  hashtpg  13839  swrdnnn0nd  14009  swrdnd0  14010  cbvsum  15044  cbvprod  15261  rpnnen2lem12  15570  lcmfpr  15961  pythagtriplem2  16144  pythagtrip  16161  mreexexd  16911  smndex1basss  18062  smndex1mgm  18064  smndex1n0mnd  18069  cnfldfunALT  20104  ppttop  21612  fixufil  22527  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  dyaddisj  24200  clwwlkneq0  27814  ofpreima2  30429  odutos  30676  trleile  30679  prmidl2  31024  prmidl0  31034  smatrcl  31149  ordtconnlem1  31277  sitgaddlemb  31716  satfvsuclem2  32720  satfvsucsuc  32725  satfdm  32729  satf0  32732  satffunlem2lem1  32764  dmopab3rexdif  32765  quad3  33026  nepss  33061  dfso2  33103  dfon2lem4  33144  dfon2lem5  33145  frrlem13  33248  dfon3  33466  brcup  33513  dfrdg4  33525  hfun  33752  bj-df-ifc  34026  bj-eltag  34413  bj-projun  34430  poimirlem22  35079  poimirlem31  35088  poimirlem32  35089  ispridl2  35476  smprngopr  35490  isdmn3  35512  sbcori  35547  tsbi4  35574  4atlem3  36892  elpadd  37095  paddasslem17  37132  cdlemg31b0N  37990  cdlemg31b0a  37991  cdlemh  38113  jm2.23  39937  ifpim123g  40208  ifpananb  40214  rp-isfinite6  40226  iunrelexp0  40403  clsk1indlem3  40746  aovov0bi  43752  zeoALTV  44188  divgcdoddALTV  44200  rrx2pnedifcoorneor  45130  line2xlem  45167