Theorem orbi12i 928

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.78  948  andir  1026  anddi  1028  cases  1058  cases2  1063  3orbi123i  1174  3or6  1476  noran  1562  cadcoma  1645  eeor  2368  neorian  3055  sspsstri  4061  rexun  4149  elsymdif  4211  indi  4237  unabw  4260  unab  4261  dfnf5  4338  ab0orv  4339  inundif  4442  dfpr2  4612  ssunsn  4796  ssunpr  4801  sspr  4802  sstp  4803  prneimg  4821  prneimg2  4822  prnebg  4823  pwpr  4868  pwtp  4869  uniun  4897  iunun  5061  iunxun  5062  brun  5164  zfpair  5394  opthneg  5465  propeqop  5492  opthprc  5727  dmopab2rex  5909  xpeq0  6159  difxp  6163  ordtri2or3  6467  ftpg  7159  ordunpr  7828  xpord2pred  8147  xpord3pred  8154  mpoxneldm  8214  tpostpos  8248  frrlem13  8301  oarec  8553  brdom2  8985  modom  9218  dfsup2  9411  wemapsolem  9519  djuunxp  9923  leweon  10011  kmlem16  10165  fin23lem40  10350  axpre-lttri  11167  nn0n0n1ge2b  12590  elnn0z  12621  fz0  13585  sqeqori  14270  hashtpg  14542  swrdnnn0nd  14718  swrdnd0  14719  cbvsum  15772  cbvsumv  15773  cbvprod  15992  cbvprodv  15993  prodeq1i  15995  rpnnen2lem12  16305  lcmfpr  16709  pythagtriplem2  16901  pythagtrip  16918  mreexexd  17728  smndex1basss  19006  smndex1mgm  19008  smndex1n0mnd  19013  opprdomnb  20867  prmidl2  21518  prmidl0  21530  cnfldfun  21588  ppttop  23216  fixufil  24132  alexsubALTlem2  24258  alexsubALTlem3  24259  alexsubALTlem4  24260  dyaddisj  25808  noetalem1  27958  addsproplem2  28216  leadds1  28235  addsuniflem  28247  addsasslem1  28249  addsasslem2  28250  negsid  28287  mulsproplem9  28370  sltmuls1  28393  sltmuls2  28394  addsdilem1  28397  addsdilem2  28398  mulsasslem1  28409  mulsasslem2  28410  precsexlem9  28461  precsexlem11  28463  clwwlkneq0  30449  ofpreima2  33084  odutos  33354  trleile  33357  domnprodeq0  33665  smatrcl  34252  ordtconnlem1  34380  sitgaddlemb  34805  satfvsuclem2  35891  satfvsucsuc  35896  satfdm  35900  satf0  35903  satffunlem2lem1  35935  dmopab3rexdif  35936  quad3  36201  nepss  36249  dfso2  36286  dfon2lem4  36315  dfon2lem5  36316  dfon3  36421  brcup  36468  dfrdg4  36482  hfun  36709  ltnadd  36749  naddle  36750  sumeq2si  36773  prodeq2si  36775  cbvprodvw2  36818  bj-df-ifc  37232  bj-eltag  37672  bj-projun  37689  poimirlem22  38352  poimirlem31  38361  poimirlem32  38362  ispridl2  38749  smprngopr  38763  isdmn3  38785  sbcori  38818  tsbi4  38845  dfsucmap3  39172  4atlem3  40430  elpadd  40633  paddasslem17  40670  cdlemg31b0N  41528  cdlemg31b0a  41529  cdlemh  41651  jm2.23  43783  ifpim123g  44286  ifpananb  44292  rp-isfinite6  44304  iunrelexp0  44488  clsk1indlem3  44829  permaxinf2lem  45781  aovov0bi  47993  zeoALTV  48495  divgcdoddALTV  48507  clnbgrsym  48663  dfclnbgr6  48681  usgrexmpl2nb0  48856  usgrexmpl2nb1  48857  usgrexmpl2nb2  48858  usgrexmpl2nb3  48859  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  usgrexmpl2trifr  48862  smprngprmrng  49163  isidom3  49169  rrx2pnedifcoorneor  49555  line2xlem  49592