Theorem orbi12i 927

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 861

This theorem is referenced by:  pm4.78  947  andir  1026  anddi  1028  cases  1058  cases2  1063  3orbi123i  1174  3or6  1476  noran  1562  cadcoma  1642  eeor  2366  neorian  3053  sspsstri  4060  rexun  4149  elsymdif  4211  indi  4237  unabw  4260  unab  4261  dfnf5  4338  ab0orv  4339  inundif  4440  dfpr2  4610  ssunsn  4794  ssunpr  4799  sspr  4800  sstp  4801  prneimg  4819  prneimg2  4820  prnebg  4821  pwpr  4866  pwtp  4867  uniun  4895  iunun  5059  iunxun  5060  brun  5162  zfpair  5392  opthneg  5463  propeqop  5490  opthprc  5725  dmopab2rex  5907  xpeq0  6157  difxp  6161  ordtri2or3  6463  ftpg  7153  ordunpr  7818  xpord2pred  8137  xpord3pred  8144  mpoxneldm  8204  tpostpos  8238  frrlem13  8291  oarec  8543  brdom2  8975  modom  9207  dfsup2  9400  wemapsolem  9508  djuunxp  9903  leweon  9991  kmlem16  10145  fin23lem40  10330  axpre-lttri  11145  nn0n0n1ge2b  12568  elnn0z  12599  fz0  13562  sqeqori  14246  hashtpg  14518  swrdnnn0nd  14690  swrdnd0  14691  cbvsum  15742  cbvsumv  15743  cbvprod  15963  cbvprodv  15964  prodeq1i  15966  rpnnen2lem12  16276  lcmfpr  16680  pythagtriplem2  16872  pythagtrip  16889  mreexexd  17699  smndex1basss  18962  smndex1mgm  18964  smndex1n0mnd  18969  opprdomnb  20815  prmidl2  21466  prmidl0  21478  cnfldfun  21536  ppttop  23164  fixufil  24079  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALTlem4  24207  dyaddisj  25755  noetalem1  27905  addsproplem2  28163  leadds1  28182  addsuniflem  28194  addsasslem1  28196  addsasslem2  28197  negsid  28234  mulsproplem9  28317  sltmuls1  28340  sltmuls2  28341  addsdilem1  28344  addsdilem2  28345  mulsasslem1  28356  mulsasslem2  28357  precsexlem9  28408  precsexlem11  28410  clwwlkneq0  30380  ofpreima2  33011  odutos  33288  trleile  33291  domnprodeq0  33599  smatrcl  34186  ordtconnlem1  34314  sitgaddlemb  34738  satfvsuclem2  35852  satfvsucsuc  35857  satfdm  35861  satf0  35864  satffunlem2lem1  35896  dmopab3rexdif  35897  quad3  36162  nepss  36210  dfso2  36247  dfon2lem4  36276  dfon2lem5  36277  dfon3  36382  brcup  36429  dfrdg4  36443  hfun  36670  ltnadd  36710  naddle  36711  sumeq2si  36734  prodeq2si  36736  cbvprodvw2  36779  bj-df-ifc  37193  bj-eltag  37633  bj-projun  37650  poimirlem22  38313  poimirlem31  38322  poimirlem32  38323  ispridl2  38709  smprngopr  38723  isdmn3  38745  sbcori  38778  tsbi4  38805  dfsucmap3  39132  4atlem3  40390  elpadd  40593  paddasslem17  40630  cdlemg31b0N  41488  cdlemg31b0a  41489  cdlemh  41611  jm2.23  43743  ifpim123g  44246  ifpananb  44252  rp-isfinite6  44264  iunrelexp0  44448  clsk1indlem3  44789  permaxinf2lem  45741  aovov0bi  47953  zeoALTV  48455  divgcdoddALTV  48467  clnbgrsym  48623  dfclnbgr6  48641  usgrexmpl2nb0  48816  usgrexmpl2nb1  48817  usgrexmpl2nb2  48818  usgrexmpl2nb3  48819  usgrexmpl2nb4  48820  usgrexmpl2nb5  48821  usgrexmpl2trifr  48822  smprngprmrng  49124  isidom3  49130  rrx2pnedifcoorneor  49516  line2xlem  49553