Theorem orbi12i 542

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

Syntax hints:   ↔ wb 195   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  pm4.78  604  andir  908  anddi  910  dfbi3  933  4exmid  977  cases  1004  3orbi123i  1245  3or6  1402  cadcoma  1542  neorian  2876  sspsstri  3671  rexun  3755  elsymdif  3811  symdif2  3814  indi  3832  unab  3853  dfnf5  3906  inundif  3998  dfpr2  4143  ssunsn  4300  ssunpr  4305  sspr  4306  sstp  4307  prneimg  4328  prnebg  4329  pwpr  4368  pwtp  4369  unipr  4385  uniun  4392  iunun  4540  iunxun  4541  brun  4633  zfpair  4831  opthneg  4876  propeqop  4895  pwunss  4943  opthprc  5089  xpeq0  5473  difxp  5477  ordtri2or3  5741  ftpg  6328  ordunpr  6918  mpt2xneldm  7225  tpostpos  7259  oarec  7529  brdom2  7871  modom  8046  dfsup2  8233  wemapsolem  8338  leweon  8717  kmlem16  8870  fin23lem40  9056  axpre-lttri  9865  nn0n0n1ge2b  11236  elnn0z  11267  fz0  12227  sqeqori  12838  hashtpg  13121  cbvsum  14273  cbvprod  14484  rpnnen2lem12  14793  lcmfpr  15178  pythagtriplem2  15360  pythagtrip  15377  mreexexd  16131  mreexexdOLD  16132  ppttop  20621  fixufil  21536  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  dyaddisj  23170  ofpreima2  28849  odutos  28994  trleile  28997  smatrcl  29190  ordtconlem1  29298  sitgaddlemb  29737  quad3  30818  nepss  30854  dfso2  30897  dfon2lem4  30935  dfon2lem5  30936  nofulllem5  31105  dfon3  31169  brcup  31216  dfrdg4  31228  hfun  31455  bj-dfifc2  31734  bj-eltag  32158  bj-projun  32175  poimirlem22  32601  poimirlem31  32610  poimirlem32  32611  ispridl2  33007  smprngopr  33021  isdmn3  33043  sbcori  33081  tsbi4  33113  4atlem3  33900  elpadd  34103  paddasslem17  34140  cdlemg31b0N  35000  cdlemg31b0a  35001  cdlemh  35123  jm2.23  36581  ifpim123g  36864  ifpananb  36870  rp-isfinite6  36883  iunrelexp0  37013  clsk1indlem3  37361  aovov0bi  39925  zeoALTV  40119  divgcdoddALTV  40131