Theorem orbi12i 914

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

Syntax hints:   ↔ wb 209   ∨ wo 846

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 847

This theorem is referenced by:  pm4.78  934  andir  1008  anddi  1010  cases  1042  cases2  1047  3orbi123i  1157  3or6  1448  noran  1531  noranOLD  1532  cadcoma  1618  neorian  3028  sspsstri  3993  rexun  4080  elsymdif  4138  indi  4164  unab  4188  dfnf5  4266  ab0orv  4267  inundif  4368  dfpr2  4535  ssunsn  4716  ssunpr  4720  sspr  4721  sstp  4722  prneimg  4740  prnebg  4741  pwpr  4790  pwtp  4791  uniprOLD  4815  uniun  4821  iunun  4978  iunxun  4979  brun  5081  zfpair  5288  opthneg  5339  propeqop  5364  pwunssOLD  5424  opthprc  5587  dmopab2rex  5760  xpeq0  5992  difxp  5996  ordtri2or3  6269  ftpg  6928  ordunpr  7560  mpoxneldm  7907  tpostpos  7941  oarec  8219  brdom2  8585  modom  8798  dfsup2  8981  wemapsolem  9087  djuunxp  9423  leweon  9511  kmlem16  9665  fin23lem40  9851  axpre-lttri  10665  nn0n0n1ge2b  12044  elnn0z  12075  fz0  13013  sqeqori  13668  hashtpg  13937  swrdnnn0nd  14107  swrdnd0  14108  cbvsum  15145  cbvprod  15361  rpnnen2lem12  15670  lcmfpr  16068  pythagtriplem2  16254  pythagtrip  16271  mreexexd  17022  smndex1basss  18186  smndex1mgm  18188  smndex1n0mnd  18193  cnfldfunALT  20230  ppttop  21758  fixufil  22673  alexsubALTlem2  22799  alexsubALTlem3  22800  alexsubALTlem4  22801  dyaddisj  24348  clwwlkneq0  27966  ofpreima2  30578  odutos  30823  trleile  30826  prmidl2  31188  prmidl0  31198  smatrcl  31318  ordtconnlem1  31446  sitgaddlemb  31885  satfvsuclem2  32893  satfvsucsuc  32898  satfdm  32902  satf0  32905  satffunlem2lem1  32937  dmopab3rexdif  32938  quad3  33199  nepss  33235  dfso2  33293  dfon2lem4  33334  dfon2lem5  33335  xpord2pred  33403  xpord3pred  33409  frrlem13  33453  noetalem1  33585  dfon3  33832  brcup  33879  dfrdg4  33891  hfun  34118  bj-df-ifc  34399  bj-eltag  34790  bj-projun  34807  poimirlem22  35422  poimirlem31  35431  poimirlem32  35432  ispridl2  35819  smprngopr  35833  isdmn3  35855  sbcori  35890  tsbi4  35917  4atlem3  37233  elpadd  37436  paddasslem17  37473  cdlemg31b0N  38331  cdlemg31b0a  38332  cdlemh  38454  jm2.23  40390  ifpim123g  40661  ifpananb  40667  rp-isfinite6  40679  iunrelexp0  40856  clsk1indlem3  41199  aovov0bi  44221  zeoALTV  44656  divgcdoddALTV  44668  rrx2pnedifcoorneor  45596  line2xlem  45633