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 275	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm4.78  934  andir  1010  anddi  1012  cases  1042  cases2  1047  3orbi123i  1156  3or6  1449  noran  1532  cadcoma  1612  eeor  2334  neorian  3027  sspsstri  4080  rexun  4171  elsymdif  4233  indi  4259  unabw  4282  unab  4283  dfnf5  4357  ab0orv  4358  inundif  4454  dfpr2  4622  ssunsn  4804  ssunpr  4810  sspr  4811  sstp  4812  prneimg  4830  prneimg2  4831  prnebg  4832  pwpr  4877  pwtp  4878  uniun  4906  iunun  5069  iunxun  5070  brun  5170  zfpair  5391  opthneg  5456  propeqop  5482  opthprc  5718  dmopab2rex  5897  xpeq0  6149  difxp  6153  ordtri2or3  6453  ftpg  7145  ordunpr  7818  xpord2pred  8142  xpord3pred  8149  mpoxneldm  8209  tpostpos  8243  frrlem13  8295  oarec  8572  brdom2  8994  modom  9250  dfsup2  9454  wemapsolem  9562  djuunxp  9933  leweon  10023  kmlem16  10178  fin23lem40  10363  axpre-lttri  11177  nn0n0n1ge2b  12568  elnn0z  12599  fz0  13554  sqeqori  14230  hashtpg  14501  swrdnnn0nd  14672  swrdnd0  14673  cbvsum  15709  cbvsumv  15710  cbvprod  15927  cbvprodv  15928  prodeq1i  15930  rpnnen2lem12  16241  lcmfpr  16644  pythagtriplem2  16835  pythagtrip  16852  mreexexd  17658  smndex1basss  18881  smndex1mgm  18883  smndex1n0mnd  18888  opprdomnb  20675  cnfldfun  21327  cnfldfunOLD  21340  ppttop  22943  fixufil  23858  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  dyaddisj  25547  noetalem1  27703  addsproplem2  27920  sleadd1  27939  addsuniflem  27951  addsasslem1  27953  addsasslem2  27954  negsid  27990  mulsproplem9  28067  ssltmul1  28090  ssltmul2  28091  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  precsexlem9  28156  precsexlem11  28158  clwwlkneq0  29956  ofpreima2  32590  odutos  32894  trleile  32897  prmidl2  33402  prmidl0  33411  smatrcl  33773  ordtconnlem1  33901  sitgaddlemb  34326  satfvsuclem2  35328  satfvsucsuc  35333  satfdm  35337  satf0  35340  satffunlem2lem1  35372  dmopab3rexdif  35373  quad3  35638  nepss  35681  dfso2  35718  dfon2lem4  35750  dfon2lem5  35751  dfon3  35856  brcup  35903  dfrdg4  35915  hfun  36142  sumeq2si  36166  prodeq2si  36168  cbvprodvw2  36211  bj-df-ifc  36544  bj-eltag  36941  bj-projun  36958  poimirlem22  37612  poimirlem31  37621  poimirlem32  37622  ispridl2  38008  smprngopr  38022  isdmn3  38044  sbcori  38079  tsbi4  38106  4atlem3  39561  elpadd  39764  paddasslem17  39801  cdlemg31b0N  40659  cdlemg31b0a  40660  cdlemh  40782  jm2.23  42967  ifpim123g  43471  ifpananb  43477  rp-isfinite6  43489  iunrelexp0  43673  clsk1indlem3  44014  permaxinf2lem  44985  aovov0bi  47173  zeoALTV  47632  divgcdoddALTV  47644  clnbgrsym  47799  dfclnbgr6  47817  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  rrx2pnedifcoorneor  48644  line2xlem  48681