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  1530  noranOLD  1531  cadcoma  1617  eeor  2333  neorian  3040  sspsstri  4041  rexun  4128  elsymdif  4186  indi  4212  unabw  4236  unab  4237  dfnf5  4316  ab0orv  4317  inundif  4417  dfpr2  4585  ssunsn  4766  ssunpr  4770  sspr  4771  sstp  4772  prneimg  4790  prnebg  4791  pwpr  4838  pwtp  4839  uniprOLD  4863  uniun  4869  iunun  5026  iunxun  5027  brun  5129  zfpair  5347  opthneg  5398  propeqop  5423  pwunssOLD  5483  opthprc  5650  dmopab2rex  5823  xpeq0  6060  difxp  6064  ordtri2or3  6360  ftpg  7022  ordunpr  7661  mpoxneldm  8012  tpostpos  8046  frrlem13  8098  oarec  8369  brdom2  8741  modom  8985  dfsup2  9164  wemapsolem  9270  djuunxp  9663  leweon  9751  kmlem16  9905  fin23lem40  10091  axpre-lttri  10905  nn0n0n1ge2b  12284  elnn0z  12315  fz0  13253  sqeqori  13911  hashtpg  14180  swrdnnn0nd  14350  swrdnd0  14351  cbvsum  15388  cbvprod  15606  rpnnen2lem12  15915  lcmfpr  16313  pythagtriplem2  16499  pythagtrip  16516  mreexexd  17338  smndex1basss  18525  smndex1mgm  18527  smndex1n0mnd  18532  cnfldfunALT  20592  ppttop  22138  fixufil  23054  alexsubALTlem2  23180  alexsubALTlem3  23181  alexsubALTlem4  23182  dyaddisj  24741  clwwlkneq0  28372  ofpreima2  30982  odutos  31225  trleile  31228  prmidl2  31595  prmidl0  31605  smatrcl  31725  ordtconnlem1  31853  sitgaddlemb  32294  satfvsuclem2  33301  satfvsucsuc  33306  satfdm  33310  satf0  33313  satffunlem2lem1  33345  dmopab3rexdif  33346  quad3  33607  nepss  33641  dfso2  33701  dfon2lem4  33741  dfon2lem5  33742  xpord2pred  33771  xpord3pred  33777  noetalem1  33923  dfon3  34173  brcup  34220  dfrdg4  34232  hfun  34459  bj-df-ifc  34740  bj-eltag  35146  bj-projun  35163  poimirlem22  35778  poimirlem31  35787  poimirlem32  35788  ispridl2  36175  smprngopr  36189  isdmn3  36211  sbcori  36246  tsbi4  36273  4atlem3  37589  elpadd  37792  paddasslem17  37829  cdlemg31b0N  38687  cdlemg31b0a  38688  cdlemh  38810  jm2.23  40798  ifpim123g  41069  ifpananb  41075  rp-isfinite6  41087  iunrelexp0  41263  clsk1indlem3  41606  aovov0bi  44639  zeoALTV  45074  divgcdoddALTV  45086  rrx2pnedifcoorneor  46014  line2xlem  46051