Theorem orbi12i 925

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

Syntax hints:   ↔ wb 208   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  pm4.78  945  andir  1022  anddi  1024  cases  1054  cases2  1059  3orbi123i  1169  3or6  1468  noran  1552  cadcoma  1632  eeor  2365  neorian  3052  sspsstri  4059  rexun  4148  elsymdif  4210  indi  4236  unabw  4259  unab  4260  dfnf5  4335  ab0orv  4336  inundif  4433  dfpr2  4603  ssunsn  4786  ssunpr  4792  sspr  4793  sstp  4794  prneimg  4812  prneimg2  4813  prnebg  4814  pwpr  4859  pwtp  4860  uniun  4888  iunun  5050  iunxun  5051  brun  5151  zfpair  5378  opthneg  5449  propeqop  5476  opthprc  5711  dmopab2rex  5893  xpeq0  6145  difxp  6149  ordtri2or3  6448  ftpg  7139  ordunpr  7806  xpord2pred  8125  xpord3pred  8132  mpoxneldm  8192  tpostpos  8226  frrlem13  8279  oarec  8531  brdom2  8963  modom  9195  dfsup2  9390  wemapsolem  9498  djuunxp  9879  leweon  9967  kmlem16  10122  fin23lem40  10308  axpre-lttri  11123  nn0n0n1ge2b  12550  elnn0z  12581  fz0  13544  sqeqori  14227  hashtpg  14498  swrdnnn0nd  14670  swrdnd0  14671  cbvsum  15722  cbvsumv  15723  cbvprod  15943  cbvprodv  15944  prodeq1i  15946  rpnnen2lem12  16257  lcmfpr  16661  pythagtriplem2  16853  pythagtrip  16870  mreexexd  17680  smndex1basss  18942  smndex1mgm  18944  smndex1n0mnd  18949  opprdomnb  20767  cnfldfun  21438  ppttop  23067  fixufil  23982  alexsubALTlem2  24108  alexsubALTlem3  24109  alexsubALTlem4  24110  dyaddisj  25658  noetalem1  27805  addsproplem2  28063  leadds1  28082  addsuniflem  28094  addsasslem1  28096  addsasslem2  28097  negsid  28134  mulsproplem9  28217  sltmuls1  28240  sltmuls2  28241  addsdilem1  28244  addsdilem2  28245  mulsasslem1  28256  mulsasslem2  28257  precsexlem9  28308  precsexlem11  28310  clwwlkneq0  30231  ofpreima2  32868  odutos  33146  trleile  33149  domnprodeq0  33460  prmidl2  33627  prmidl0  33637  smatrcl  34093  ordtconnlem1  34221  sitgaddlemb  34645  satfvsuclem2  35710  satfvsucsuc  35715  satfdm  35719  satf0  35722  satffunlem2lem1  35754  dmopab3rexdif  35755  quad3  36020  nepss  36068  dfso2  36105  dfon2lem4  36134  dfon2lem5  36135  dfon3  36240  brcup  36287  dfrdg4  36301  hfun  36528  sumeq2si  36562  prodeq2si  36564  cbvprodvw2  36607  bj-df-ifc  37023  bj-eltag  37462  bj-projun  37479  poimirlem22  38141  poimirlem31  38150  poimirlem32  38151  ispridl2  38537  smprngopr  38551  isdmn3  38573  sbcori  38608  tsbi4  38635  dfsucmap3  38962  4atlem3  40220  elpadd  40423  paddasslem17  40460  cdlemg31b0N  41318  cdlemg31b0a  41319  cdlemh  41441  jm2.23  43573  ifpim123g  44076  ifpananb  44082  rp-isfinite6  44094  iunrelexp0  44278  clsk1indlem3  44619  permaxinf2lem  45588  aovov0bi  47790  zeoALTV  48292  divgcdoddALTV  48304  clnbgrsym  48460  dfclnbgr6  48478  usgrexmpl2nb0  48653  usgrexmpl2nb1  48654  usgrexmpl2nb2  48655  usgrexmpl2nb3  48656  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  usgrexmpl2trifr  48659  rrx2pnedifcoorneor  49338  line2xlem  49375