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 845

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 846

This theorem is referenced by:  pm4.78  933  andir  1007  anddi  1009  cases  1041  cases2  1046  3orbi123i  1156  3or6  1447  noran  1531  cadcoma  1611  eeor  2328  neorian  3037  sspsstri  4043  rexun  4130  elsymdif  4187  indi  4213  unabw  4237  unab  4238  dfnf5  4317  ab0orv  4318  inundif  4418  dfpr2  4584  ssunsn  4767  ssunpr  4771  sspr  4772  sstp  4773  prneimg  4791  prnebg  4792  pwpr  4838  pwtp  4839  uniprOLD  4863  uniun  4870  iunun  5029  iunxun  5030  brun  5132  zfpair  5353  opthneg  5409  propeqop  5434  opthprc  5662  dmopab2rex  5839  xpeq0  6078  difxp  6082  ordtri2or3  6380  ftpg  7060  ordunpr  7705  mpoxneldm  8059  tpostpos  8093  frrlem13  8145  oarec  8424  brdom2  8803  modom  9065  dfsup2  9247  wemapsolem  9353  djuunxp  9723  leweon  9813  kmlem16  9967  fin23lem40  10153  axpre-lttri  10967  nn0n0n1ge2b  12347  elnn0z  12378  fz0  13317  sqeqori  13976  hashtpg  14244  swrdnnn0nd  14414  swrdnd0  14415  cbvsum  15452  cbvprod  15670  rpnnen2lem12  15979  lcmfpr  16377  pythagtriplem2  16563  pythagtrip  16580  mreexexd  17402  smndex1basss  18589  smndex1mgm  18591  smndex1n0mnd  18596  cnfldfun  20654  ppttop  22202  fixufil  23118  alexsubALTlem2  23244  alexsubALTlem3  23245  alexsubALTlem4  23246  dyaddisj  24805  clwwlkneq0  28438  ofpreima2  31048  odutos  31291  trleile  31294  prmidl2  31661  prmidl0  31671  smatrcl  31791  ordtconnlem1  31919  sitgaddlemb  32360  satfvsuclem2  33367  satfvsucsuc  33372  satfdm  33376  satf0  33379  satffunlem2lem1  33411  dmopab3rexdif  33412  quad3  33673  nepss  33707  dfso2  33767  dfon2lem4  33807  dfon2lem5  33808  xpord2pred  33837  xpord3pred  33843  noetalem1  33989  dfon3  34239  brcup  34286  dfrdg4  34298  hfun  34525  bj-df-ifc  34806  bj-eltag  35211  bj-projun  35228  poimirlem22  35843  poimirlem31  35852  poimirlem32  35853  ispridl2  36240  smprngopr  36254  isdmn3  36276  sbcori  36311  tsbi4  36338  4atlem3  37652  elpadd  37855  paddasslem17  37892  cdlemg31b0N  38750  cdlemg31b0a  38751  cdlemh  38873  jm2.23  40856  ifpim123g  41145  ifpananb  41151  rp-isfinite6  41163  iunrelexp0  41348  clsk1indlem3  41691  aovov0bi  44746  zeoALTV  45180  divgcdoddALTV  45192  rrx2pnedifcoorneor  46120  line2xlem  46157