Theorem orbi12i 928

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.78  948  andir  1026  anddi  1028  cases  1058  cases2  1063  3orbi123i  1174  3or6  1476  noran  1561  cadcoma  1644  eeor  2363  neorian  3050  sspsstri  4032  rexun  4193  elsymdif  4202  indi  4228  unabw  4251  unab  4252  dfnf5  4330  ab0orv  4331  inundif  4434  dfpr2  4601  ssunsn  4783  ssunpr  4788  sspr  4789  sstp  4790  prneimg  4808  prneimg2  4809  prnebg  4810  pwpr  4827  pwtp  4828  uniun  4889  iunun  5052  iunxun  5053  brun  5155  zfpair  5383  opthneg  5450  propeqop  5479  opthprc  5715  dmopab2rex  5900  xpeq0  6153  difxp  6157  ordtri2or3  6468  ftpg  7165  ordunpr  7841  xpord2pred  8169  xpord3pred  8176  mpoxneldm  8237  tpostpos  8271  frrlem13  8324  oarec  8578  brdom2  9017  modom  9250  dfsup2  9443  wemapsolem  9551  hfunOLD  9926  djuunxp  10009  leweon  10097  kmlem16  10251  fin23lem40  10436  axpre-lttri  11257  nn0n0n1ge2b  12682  elnn0z  12713  fz0  13679  sqeqori  14365  hashtpg  14637  swrdnnn0nd  14814  swrdnd0  14815  cbvsum  15871  cbvsumv  15872  cbvprod  16091  cbvprodv  16092  prodeq1i  16094  rpnnen2lem12  16402  lcmfpr  16811  pythagtriplem2  17004  pythagtrip  17021  mreexexd  17831  smndex1basss  19113  smndex1mgm  19115  smndex1n0mnd  19120  opprdomnb  20977  prmidl2  21631  prmidl0  21643  cnfldfun  21701  ppttop  23334  fixufil  24250  alexsubALTlem2  24376  alexsubALTlem3  24377  alexsubALTlem4  24378  dyaddisj  25926  noetalem1  28107  addsproplem2  28365  leadds1  28384  addsuniflem  28396  addsasslem1  28398  addsasslem2  28399  negsid  28436  mulsproplem9  28519  sltmuls1  28542  sltmuls2  28543  addsdilem1  28546  addsdilem2  28547  mulsasslem1  28558  mulsasslem2  28559  precsexlem9  28610  precsexlem11  28612  clwwlkneq0  30629  ofpreima2  33311  odutos  33579  trleile  33582  domnprodeq0  33890  smatrcl  34478  ordtconnlem1  34606  sitgaddlemb  35030  satfvsuclem2  36243  satfvsucsuc  36248  satfdm  36252  satf0  36255  satffunlem2lem1  36287  dmopab3rexdif  36288  quad3  36553  nepss  36607  dfso2  36644  dfon2lem4  36672  dfon2lem5  36673  dfon3  36778  brcup  36825  dfrdg4  36839  ltnadd  37091  naddle  37092  sumeq2si  37115  prodeq2si  37117  cbvprodvw2  37160  bj-df-ifc  37574  bj-eltag  38014  bj-projun  38031  poimirlem22  38697  poimirlem31  38706  poimirlem32  38707  ispridl2  39109  smprngopr  39123  isdmn3  39145  sbcori  39178  tsbi4  39205  dfsucmap3  39532  4atlem3  40790  elpadd  40993  paddasslem17  41030  cdlemg31b0N  41888  cdlemg31b0a  41889  cdlemh  42011  jm2.23  44140  ifpim123g  44638  ifpananb  44644  rp-isfinite6  44656  iunrelexp0  44839  clsk1indlem3  45180  permaxinf2lem  46138  aovov0bi  48402  zeoALTV  48904  divgcdoddALTV  48916  clnbgrsym  49072  dfclnbgr6  49090  usgrexmpl2nb0  49265  usgrexmpl2nb1  49266  usgrexmpl2nb2  49267  usgrexmpl2nb3  49268  usgrexmpl2nb4  49269  usgrexmpl2nb5  49270  usgrexmpl2trifr  49271  smprngprmrng  49572  isidom3  49578  rrx2pnedifcoorneor  49965  line2xlem  50001  parhomel  50880