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  3037  sspsstri  4102  rexun  4190  elsymdif  4247  indi  4273  unabw  4297  unab  4298  dfnf5  4377  ab0orv  4378  inundif  4478  dfpr2  4647  ssunsn  4831  ssunpr  4835  sspr  4836  sstp  4837  prneimg  4855  prnebg  4856  pwpr  4902  pwtp  4903  uniprOLD  4927  uniun  4934  iunun  5096  iunxun  5097  brun  5199  zfpair  5419  opthneg  5481  propeqop  5507  opthprc  5740  dmopab2rex  5917  xpeq0  6159  difxp  6163  ordtri2or3  6464  ftpg  7156  ordunpr  7816  xpord2pred  8133  xpord3pred  8140  mpoxneldm  8199  tpostpos  8233  frrlem13  8285  oarec  8564  brdom2  8980  modom  9246  dfsup2  9441  wemapsolem  9547  djuunxp  9918  leweon  10008  kmlem16  10162  fin23lem40  10348  axpre-lttri  11162  nn0n0n1ge2b  12542  elnn0z  12573  fz0  13518  sqeqori  14180  hashtpg  14448  swrdnnn0nd  14608  swrdnd0  14609  cbvsum  15643  cbvprod  15861  rpnnen2lem12  16170  lcmfpr  16566  pythagtriplem2  16752  pythagtrip  16769  mreexexd  17594  smndex1basss  18788  smndex1mgm  18790  smndex1n0mnd  18795  cnfldfun  20962  ppttop  22517  fixufil  23433  alexsubALTlem2  23559  alexsubALTlem3  23560  alexsubALTlem4  23561  dyaddisj  25120  noetalem1  27251  addsproplem2  27463  sleadd1  27482  addsuniflem  27494  addsasslem1  27496  addsasslem2  27497  negsid  27525  mulsproplem9  27590  ssltmul1  27612  ssltmul2  27613  addsdilem1  27616  addsdilem2  27617  mulsasslem1  27628  mulsasslem2  27629  precsexlem9  27671  precsexlem11  27673  clwwlkneq0  29320  ofpreima2  31929  odutos  32176  trleile  32179  prmidl2  32604  prmidl0  32614  smatrcl  32845  ordtconnlem1  32973  sitgaddlemb  33416  satfvsuclem2  34420  satfvsucsuc  34425  satfdm  34429  satf0  34432  satffunlem2lem1  34464  dmopab3rexdif  34465  quad3  34724  nepss  34756  dfso2  34794  dfon2lem4  34827  dfon2lem5  34828  dfon3  34933  brcup  34980  dfrdg4  34992  hfun  35219  gg-cnfldfun  35266  bj-df-ifc  35543  bj-eltag  35944  bj-projun  35961  poimirlem22  36596  poimirlem31  36605  poimirlem32  36606  ispridl2  36992  smprngopr  37006  isdmn3  37028  sbcori  37063  tsbi4  37090  4atlem3  38553  elpadd  38756  paddasslem17  38793  cdlemg31b0N  39651  cdlemg31b0a  39652  cdlemh  39774  jm2.23  41817  ifpim123g  42333  ifpananb  42339  rp-isfinite6  42351  iunrelexp0  42535  clsk1indlem3  42876  aovov0bi  45983  zeoALTV  46417  divgcdoddALTV  46429  rrx2pnedifcoorneor  47480  line2xlem  47517