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

Syntax hints:   ↔ wb 205   ∨ 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 206  df-or 847

This theorem is referenced by:  pm4.78  933  andir  1007  anddi  1009  cases  1041  cases2  1046  3orbi123i  1154  3or6  1444  noran  1526  cadcoma  1606  eeor  2324  neorian  3032  sspsstri  4098  rexun  4186  elsymdif  4243  indi  4269  unabw  4293  unab  4294  dfnf5  4373  ab0orv  4374  inundif  4474  dfpr2  4643  ssunsn  4827  ssunpr  4831  sspr  4832  sstp  4833  prneimg  4851  prnebg  4852  pwpr  4897  pwtp  4898  uniprOLD  4921  uniun  4928  iunun  5090  iunxun  5091  brun  5193  zfpair  5415  opthneg  5477  propeqop  5503  opthprc  5736  dmopab2rex  5914  xpeq0  6158  difxp  6162  ordtri2or3  6463  ftpg  7159  ordunpr  7823  xpord2pred  8144  xpord3pred  8151  mpoxneldm  8211  tpostpos  8245  frrlem13  8297  oarec  8576  brdom2  8994  modom  9260  dfsup2  9459  wemapsolem  9565  djuunxp  9936  leweon  10026  kmlem16  10180  fin23lem40  10366  axpre-lttri  11180  nn0n0n1ge2b  12562  elnn0z  12593  fz0  13540  sqeqori  14201  hashtpg  14470  swrdnnn0nd  14630  swrdnd0  14631  cbvsum  15665  cbvprod  15883  rpnnen2lem12  16193  lcmfpr  16589  pythagtriplem2  16777  pythagtrip  16794  mreexexd  17619  smndex1basss  18848  smndex1mgm  18850  smndex1n0mnd  18855  cnfldfun  21280  cnfldfunOLD  21293  ppttop  22897  fixufil  23813  alexsubALTlem2  23939  alexsubALTlem3  23940  alexsubALTlem4  23941  dyaddisj  25512  noetalem1  27661  addsproplem2  27874  sleadd1  27893  addsuniflem  27905  addsasslem1  27907  addsasslem2  27908  negsid  27940  mulsproplem9  28011  ssltmul1  28034  ssltmul2  28035  addsdilem1  28038  addsdilem2  28039  mulsasslem1  28050  mulsasslem2  28051  precsexlem9  28100  precsexlem11  28102  clwwlkneq0  29826  ofpreima2  32435  odutos  32677  trleile  32680  prmidl2  33092  prmidl0  33102  smatrcl  33333  ordtconnlem1  33461  sitgaddlemb  33904  satfvsuclem2  34906  satfvsucsuc  34911  satfdm  34915  satf0  34918  satffunlem2lem1  34950  dmopab3rexdif  34951  quad3  35210  nepss  35248  dfso2  35285  dfon2lem4  35318  dfon2lem5  35319  dfon3  35424  brcup  35471  dfrdg4  35483  hfun  35710  bj-df-ifc  35992  bj-eltag  36392  bj-projun  36409  poimirlem22  37050  poimirlem31  37059  poimirlem32  37060  ispridl2  37446  smprngopr  37460  isdmn3  37482  sbcori  37517  tsbi4  37544  4atlem3  39006  elpadd  39209  paddasslem17  39246  cdlemg31b0N  40104  cdlemg31b0a  40105  cdlemh  40227  jm2.23  42339  ifpim123g  42853  ifpananb  42859  rp-isfinite6  42871  iunrelexp0  43055  clsk1indlem3  43396  aovov0bi  46499  zeoALTV  46933  divgcdoddALTV  46945  rrx2pnedifcoorneor  47712  line2xlem  47749