Theorem orbi12i 913

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

Syntax hints:   ↔ wb 205   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  pm4.78  933  andir  1007  anddi  1009  cases  1041  cases2  1046  3orbi123i  1156  3or6  1447  noran  1533  cadcoma  1613  eeor  2329  neorian  3036  sspsstri  4067  rexun  4155  elsymdif  4212  indi  4238  unabw  4262  unab  4263  dfnf5  4342  ab0orv  4343  inundif  4443  dfpr2  4610  ssunsn  4793  ssunpr  4797  sspr  4798  sstp  4799  prneimg  4817  prnebg  4818  pwpr  4864  pwtp  4865  uniprOLD  4889  uniun  4896  iunun  5058  iunxun  5059  brun  5161  zfpair  5381  opthneg  5443  propeqop  5469  opthprc  5701  dmopab2rex  5878  xpeq0  6117  difxp  6121  ordtri2or3  6422  ftpg  7107  ordunpr  7766  xpord2pred  8082  xpord3pred  8089  mpoxneldm  8148  tpostpos  8182  frrlem13  8234  oarec  8514  brdom2  8929  modom  9195  dfsup2  9389  wemapsolem  9495  djuunxp  9866  leweon  9956  kmlem16  10110  fin23lem40  10296  axpre-lttri  11110  nn0n0n1ge2b  12490  elnn0z  12521  fz0  13466  sqeqori  14128  hashtpg  14396  swrdnnn0nd  14556  swrdnd0  14557  cbvsum  15591  cbvprod  15809  rpnnen2lem12  16118  lcmfpr  16514  pythagtriplem2  16700  pythagtrip  16717  mreexexd  17542  smndex1basss  18729  smndex1mgm  18731  smndex1n0mnd  18736  cnfldfun  20845  ppttop  22394  fixufil  23310  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALTlem4  23438  dyaddisj  24997  noetalem1  27126  addsproplem2  27325  sleadd1  27341  addsunif  27353  addsasslem1  27354  addsasslem2  27355  negsid  27382  mulsproplem10  27431  clwwlkneq0  29036  ofpreima2  31649  odutos  31898  trleile  31901  prmidl2  32289  prmidl0  32299  smatrcl  32466  ordtconnlem1  32594  sitgaddlemb  33037  satfvsuclem2  34041  satfvsucsuc  34046  satfdm  34050  satf0  34053  satffunlem2lem1  34085  dmopab3rexdif  34086  quad3  34345  nepss  34376  dfso2  34414  dfon2lem4  34447  dfon2lem5  34448  dfon3  34553  brcup  34600  dfrdg4  34612  hfun  34839  bj-df-ifc  35120  bj-eltag  35521  bj-projun  35538  poimirlem22  36173  poimirlem31  36182  poimirlem32  36183  ispridl2  36570  smprngopr  36584  isdmn3  36606  sbcori  36641  tsbi4  36668  4atlem3  38132  elpadd  38335  paddasslem17  38372  cdlemg31b0N  39230  cdlemg31b0a  39231  cdlemh  39353  jm2.23  41378  ifpim123g  41894  ifpananb  41900  rp-isfinite6  41912  iunrelexp0  42096  clsk1indlem3  42437  aovov0bi  45548  zeoALTV  45982  divgcdoddALTV  45994  rrx2pnedifcoorneor  46922  line2xlem  46959