Theorem orbi12i 911

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

Syntax hints:   ↔ wb 205   ∨ wo 843

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 844

This theorem is referenced by:  pm4.78  931  andir  1005  anddi  1007  cases  1039  cases2  1044  3orbi123i  1154  3or6  1445  noran  1531  cadcoma  1611  eeor  2327  neorian  3035  sspsstri  4101  rexun  4189  elsymdif  4246  indi  4272  unabw  4296  unab  4297  dfnf5  4376  ab0orv  4377  inundif  4477  dfpr2  4646  ssunsn  4830  ssunpr  4834  sspr  4835  sstp  4836  prneimg  4854  prnebg  4855  pwpr  4901  pwtp  4902  uniprOLD  4926  uniun  4933  iunun  5095  iunxun  5096  brun  5198  zfpair  5418  opthneg  5480  propeqop  5506  opthprc  5739  dmopab2rex  5916  xpeq0  6158  difxp  6162  ordtri2or3  6463  ftpg  7155  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  12544  elnn0z  12575  fz0  13520  sqeqori  14182  hashtpg  14450  swrdnnn0nd  14610  swrdnd0  14611  cbvsum  15645  cbvprod  15863  rpnnen2lem12  16172  lcmfpr  16568  pythagtriplem2  16754  pythagtrip  16771  mreexexd  17596  smndex1basss  18822  smndex1mgm  18824  smndex1n0mnd  18829  cnfldfun  21156  ppttop  22730  fixufil  23646  alexsubALTlem2  23772  alexsubALTlem3  23773  alexsubALTlem4  23774  dyaddisj  25345  noetalem1  27480  addsproplem2  27692  sleadd1  27711  addsuniflem  27723  addsasslem1  27725  addsasslem2  27726  negsid  27754  mulsproplem9  27819  ssltmul1  27841  ssltmul2  27842  addsdilem1  27845  addsdilem2  27846  mulsasslem1  27857  mulsasslem2  27858  precsexlem9  27900  precsexlem11  27902  clwwlkneq0  29549  ofpreima2  32158  odutos  32405  trleile  32408  prmidl2  32833  prmidl0  32843  smatrcl  33074  ordtconnlem1  33202  sitgaddlemb  33645  satfvsuclem2  34649  satfvsucsuc  34654  satfdm  34658  satf0  34661  satffunlem2lem1  34693  dmopab3rexdif  34694  quad3  34953  nepss  34991  dfso2  35029  dfon2lem4  35062  dfon2lem5  35063  dfon3  35168  brcup  35215  dfrdg4  35227  hfun  35454  gg-cnfldfun  35483  bj-df-ifc  35760  bj-eltag  36161  bj-projun  36178  poimirlem22  36813  poimirlem31  36822  poimirlem32  36823  ispridl2  37209  smprngopr  37223  isdmn3  37245  sbcori  37280  tsbi4  37307  4atlem3  38770  elpadd  38973  paddasslem17  39010  cdlemg31b0N  39868  cdlemg31b0a  39869  cdlemh  39991  jm2.23  42037  ifpim123g  42553  ifpananb  42559  rp-isfinite6  42571  iunrelexp0  42755  clsk1indlem3  43096  aovov0bi  46202  zeoALTV  46636  divgcdoddALTV  46648  rrx2pnedifcoorneor  47489  line2xlem  47526