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  1477  noran  1562  cadcoma  1645  eeor  2367  neorian  3054  sspsstri  4036  rexun  4197  elsymdif  4206  indi  4232  unabw  4255  unab  4256  dfnf5  4334  ab0orv  4335  inundif  4438  dfpr2  4605  ssunsn  4789  ssunpr  4794  sspr  4795  sstp  4796  prneimg  4814  prneimg2  4815  prnebg  4816  pwpr  4833  pwtp  4834  uniun  4895  iunun  5058  iunxun  5059  brun  5162  zfpair  5390  opthneg  5457  propeqop  5486  opthprc  5722  dmopab2rex  5911  xpeq0  6169  difxp  6173  ordtri2or3  6491  ftpg  7192  ordunpr  7871  xpord2pred  8199  xpord3pred  8206  mpoxneldm  8267  tpostpos  8301  frrlem13  8354  oarec  8608  brdom2  9047  modom  9280  dfsup2  9473  wemapsolem  9581  hfunOLD  9956  djuunxp  10039  leweon  10129  kmlem16  10283  fin23lem40  10468  axpre-lttri  11289  nn0n0n1ge2b  12715  elnn0z  12746  fz0  13712  sqeqori  14399  hashtpg  14671  swrdnnn0nd  14848  swrdnd0  14849  cbvsum  15906  cbvsumv  15907  cbvprod  16126  cbvprodv  16127  prodeq1i  16129  rpnnen2lem12  16437  lcmfpr  16846  pythagtriplem2  17039  pythagtrip  17056  mreexexd  17872  smndex1basss  19154  smndex1mgm  19156  smndex1n0mnd  19161  opprdomnb  21019  prmidl2  21673  prmidl0  21685  cnfldfun  21744  ppttop  23380  fixufil  24296  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALTlem4  24424  dyaddisj  25972  noetalem1  28155  addsproplem2  28413  leadds1  28432  addsuniflem  28444  addsasslem1  28446  addsasslem2  28447  negsid  28484  mulsproplem9  28567  sltmuls1  28590  sltmuls2  28591  addsdilem1  28594  addsdilem2  28595  mulsasslem1  28606  mulsasslem2  28607  precsexlem9  28658  precsexlem11  28660  clwwlkneq0  30677  ofpreima2  33358  odutos  33625  trleile  33628  domnprodeq0  33939  smatrcl  34539  ordtconnlem1  34667  sitgaddlemb  35091  satfvsuclem2  36333  satfvsucsuc  36338  satfdm  36342  satf0  36345  satffunlem2lem1  36377  dmopab3rexdif  36378  quad3  36643  nepss  36698  dfso2  36735  dfon2lem4  36763  dfon2lem5  36764  dfon3  36869  brcup  36916  dfrdg4  36930  ltnadd  37182  naddle  37183  sumeq2si  37206  prodeq2si  37208  cbvprodvw2  37251  bj-df-ifc  37665  bj-eltag  38105  bj-projun  38122  poimirlem22  38828  poimirlem31  38837  poimirlem32  38838  ispridl2  39238  smprngopr  39252  isdmn3  39274  sbcori  39307  tsbi4  39334  dfsucmap3  39661  4atlem3  40919  elpadd  41122  paddasslem17  41159  cdlemg31b0N  42017  cdlemg31b0a  42018  cdlemh  42140  jm2.23  44269  ifpim123g  44762  ifpananb  44768  rp-isfinite6  44780  iunrelexp0  44963  clsk1indlem3  45304  permaxinf2lem  46266  aovov0bi  48539  zeoALTV  49041  divgcdoddALTV  49053  clnbgrsym  49209  dfclnbgr6  49227  usgrexmpl2nb0  49402  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  usgrexmpl2trifr  49408  smprngprmrng  49767  isidom3  49773  rrx2pnedifcoorneor  50160  line2xlem  50196  parhomel  51075